elicitation/verification/types/
tuples.rs

1//! Tuple contract types demonstrating compositional verification.
2//!
3//! Tuples compose contract types - if all elements are valid contract types,
4//! the tuple is guaranteed valid by construction.
5
6use crate::{ElicitCommunicator, ElicitResult, Elicitation, Prompt};
7
8// Tuple2 - 2-element tuple where both satisfy contracts
9/// A 2-element tuple where both elements are contract types.
10///
11/// **Compositional verification:** If C1 and C2 are valid contracts,
12/// Tuple2<C1, C2> is automatically valid by construction.
13#[derive(Debug, Clone, PartialEq, Eq, Hash)]
14pub struct Tuple2<C1, C2>(pub C1, pub C2);
15
16impl<C1, C2> Tuple2<C1, C2> {
17    /// Create a new Tuple2. Both elements are already validated contract types.
18    pub fn new(first: C1, second: C2) -> Self {
19        Self(first, second)
20    }
21
22    /// Get the first element.
23    pub fn first(&self) -> &C1 {
24        &self.0
25    }
26
27    /// Get the second element.
28    pub fn second(&self) -> &C2 {
29        &self.1
30    }
31
32    /// Unwrap into components.
33    pub fn into_inner(self) -> (C1, C2) {
34        (self.0, self.1)
35    }
36}
37
38impl<C1, C2> Prompt for Tuple2<C1, C2>
39where
40    C1: Elicitation + Send,
41    C2: Elicitation + Send,
42{
43    fn prompt() -> Option<&'static str> {
44        Some("Eliciting tuple with 2 elements:")
45    }
46}
47
48impl<C1, C2> Elicitation for Tuple2<C1, C2>
49where
50    C1: Elicitation + Send,
51    C2: Elicitation + Send,
52{
53    type Style = <(C1, C2) as Elicitation>::Style;
54
55    #[tracing::instrument(skip(communicator))]
56    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
57        tracing::debug!("Eliciting Tuple2");
58        let first = C1::elicit(communicator).await?; // Guaranteed valid by contract!
59        let second = C2::elicit(communicator).await?; // Guaranteed valid by contract!
60        Ok(Self::new(first, second)) // Composition = proven valid
61    }
62
63    fn kani_proof() -> proc_macro2::TokenStream {
64        proc_macro2::TokenStream::new()
65    }
66
67    fn verus_proof() -> proc_macro2::TokenStream {
68        proc_macro2::TokenStream::new()
69    }
70
71    fn creusot_proof() -> proc_macro2::TokenStream {
72        proc_macro2::TokenStream::new()
73    }
74}
75
76// Tuple3 - 3-element tuple
77/// A 3-element tuple where all elements are contract types.
78#[derive(Debug, Clone, PartialEq, Eq, Hash)]
79pub struct Tuple3<C1, C2, C3>(pub C1, pub C2, pub C3);
80
81impl<C1, C2, C3> Tuple3<C1, C2, C3> {
82    /// Create a new Tuple3.
83    pub fn new(first: C1, second: C2, third: C3) -> Self {
84        Self(first, second, third)
85    }
86
87    /// Unwrap into components.
88    pub fn into_inner(self) -> (C1, C2, C3) {
89        (self.0, self.1, self.2)
90    }
91}
92
93impl<C1, C2, C3> Prompt for Tuple3<C1, C2, C3>
94where
95    C1: Elicitation + Send,
96    C2: Elicitation + Send,
97    C3: Elicitation + Send,
98{
99    fn prompt() -> Option<&'static str> {
100        Some("Eliciting tuple with 3 elements:")
101    }
102}
103
104impl<C1, C2, C3> Elicitation for Tuple3<C1, C2, C3>
105where
106    C1: Elicitation + Send,
107    C2: Elicitation + Send,
108    C3: Elicitation + Send,
109{
110    type Style = <(C1, C2, C3) as Elicitation>::Style;
111
112    #[tracing::instrument(skip(communicator))]
113    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
114        tracing::debug!("Eliciting Tuple3");
115        let first = C1::elicit(communicator).await?;
116        let second = C2::elicit(communicator).await?;
117        let third = C3::elicit(communicator).await?;
118        Ok(Self::new(first, second, third))
119    }
120
121    fn kani_proof() -> proc_macro2::TokenStream {
122        proc_macro2::TokenStream::new()
123    }
124
125    fn verus_proof() -> proc_macro2::TokenStream {
126        proc_macro2::TokenStream::new()
127    }
128
129    fn creusot_proof() -> proc_macro2::TokenStream {
130        proc_macro2::TokenStream::new()
131    }
132}
133
134// Tuple4 - 4-element tuple
135/// A 4-element tuple where all elements are contract types.
136#[derive(Debug, Clone, PartialEq, Eq, Hash)]
137pub struct Tuple4<C1, C2, C3, C4>(pub C1, pub C2, pub C3, pub C4);
138
139impl<C1, C2, C3, C4> Tuple4<C1, C2, C3, C4> {
140    /// Create a new Tuple4.
141    pub fn new(first: C1, second: C2, third: C3, fourth: C4) -> Self {
142        Self(first, second, third, fourth)
143    }
144
145    /// Unwrap into components.
146    pub fn into_inner(self) -> (C1, C2, C3, C4) {
147        (self.0, self.1, self.2, self.3)
148    }
149}
150
151impl<C1, C2, C3, C4> Prompt for Tuple4<C1, C2, C3, C4>
152where
153    C1: Elicitation + Send,
154    C2: Elicitation + Send,
155    C3: Elicitation + Send,
156    C4: Elicitation + Send,
157{
158    fn prompt() -> Option<&'static str> {
159        Some("Eliciting tuple with 4 elements:")
160    }
161}
162
163impl<C1, C2, C3, C4> Elicitation for Tuple4<C1, C2, C3, C4>
164where
165    C1: Elicitation + Send,
166    C2: Elicitation + Send,
167    C3: Elicitation + Send,
168    C4: Elicitation + Send,
169{
170    type Style = <(C1, C2, C3, C4) as Elicitation>::Style;
171
172    #[tracing::instrument(skip(communicator))]
173    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
174        tracing::debug!("Eliciting Tuple4");
175        let first = C1::elicit(communicator).await?;
176        let second = C2::elicit(communicator).await?;
177        let third = C3::elicit(communicator).await?;
178        let fourth = C4::elicit(communicator).await?;
179        Ok(Self::new(first, second, third, fourth))
180    }
181
182    fn kani_proof() -> proc_macro2::TokenStream {
183        proc_macro2::TokenStream::new()
184    }
185
186    fn verus_proof() -> proc_macro2::TokenStream {
187        proc_macro2::TokenStream::new()
188    }
189
190    fn creusot_proof() -> proc_macro2::TokenStream {
191        proc_macro2::TokenStream::new()
192    }
193}
194
195#[cfg(test)]
196mod tests {
197    use super::*;
198    use crate::verification::types::{BoolTrue, I8Positive, StringNonEmpty};
199
200    #[test]
201    fn test_tuple2_new() {
202        let s: StringNonEmpty = StringNonEmpty::new("test".to_string()).unwrap();
203        let t = Tuple2::new(I8Positive::new(5).unwrap(), s);
204        assert_eq!(t.first().get(), 5);
205        assert_eq!(t.second().get(), "test");
206    }
207
208    #[test]
209    fn test_tuple2_into_inner() {
210        let s: StringNonEmpty = StringNonEmpty::new("test".to_string()).unwrap();
211        let t = Tuple2::new(I8Positive::new(5).unwrap(), s);
212        let (first, second) = t.into_inner();
213        assert_eq!(first.get(), 5);
214        assert_eq!(second.get(), "test");
215    }
216
217    #[test]
218    fn test_tuple3_new() {
219        let s: StringNonEmpty = StringNonEmpty::new("test".to_string()).unwrap();
220        let t = Tuple3::new(I8Positive::new(5).unwrap(), s, BoolTrue::new(true).unwrap());
221        let (first, second, third) = t.into_inner();
222        assert_eq!(first.get(), 5);
223        assert_eq!(second.get(), "test");
224        assert!(third.get());
225    }
226
227    #[test]
228    fn test_tuple4_new() {
229        let t = Tuple4::new(
230            I8Positive::new(1).unwrap(),
231            I8Positive::new(2).unwrap(),
232            I8Positive::new(3).unwrap(),
233            I8Positive::new(4).unwrap(),
234        );
235        let (a, b, c, d) = t.into_inner();
236        assert_eq!(a.get(), 1);
237        assert_eq!(b.get(), 2);
238        assert_eq!(c.get(), 3);
239        assert_eq!(d.get(), 4);
240    }
241}
242
243// ── Serde + JsonSchema impls ──────────────────────────────────────────────────
244
245impl<C1: serde::Serialize, C2: serde::Serialize> serde::Serialize for Tuple2<C1, C2> {
246    fn serialize<S: serde::Serializer>(&self, s: S) -> Result<S::Ok, S::Error> {
247        (&self.0, &self.1).serialize(s)
248    }
249}
250
251impl<'de, C1: serde::Deserialize<'de>, C2: serde::Deserialize<'de>> serde::Deserialize<'de>
252    for Tuple2<C1, C2>
253{
254    fn deserialize<D: serde::Deserializer<'de>>(d: D) -> Result<Self, D::Error> {
255        let (c1, c2) = <(C1, C2)>::deserialize(d)?;
256        Ok(Self(c1, c2))
257    }
258}
259
260impl<C1: schemars::JsonSchema, C2: schemars::JsonSchema> schemars::JsonSchema for Tuple2<C1, C2> {
261    fn schema_name() -> ::std::borrow::Cow<'static, str> {
262        format!("Tuple2<{},{}>", C1::schema_name(), C2::schema_name()).into()
263    }
264    fn json_schema(generator: &mut schemars::SchemaGenerator) -> schemars::Schema {
265        let c1_val = serde_json::to_value(generator.subschema_for::<C1>()).expect("schema");
266        let c2_val = serde_json::to_value(generator.subschema_for::<C2>()).expect("schema");
267        let mut map = serde_json::Map::new();
268        map.insert("type".to_string(), "array".into());
269        map.insert("minItems".to_string(), 2u64.into());
270        map.insert("maxItems".to_string(), 2u64.into());
271        map.insert(
272            "prefixItems".to_string(),
273            serde_json::Value::Array(vec![c1_val, c2_val]),
274        );
275        schemars::Schema::from(map)
276    }
277}
278
279impl<C1: serde::Serialize, C2: serde::Serialize, C3: serde::Serialize> serde::Serialize
280    for Tuple3<C1, C2, C3>
281{
282    fn serialize<S: serde::Serializer>(&self, s: S) -> Result<S::Ok, S::Error> {
283        (&self.0, &self.1, &self.2).serialize(s)
284    }
285}
286
287impl<'de, C1: serde::Deserialize<'de>, C2: serde::Deserialize<'de>, C3: serde::Deserialize<'de>>
288    serde::Deserialize<'de> for Tuple3<C1, C2, C3>
289{
290    fn deserialize<D: serde::Deserializer<'de>>(d: D) -> Result<Self, D::Error> {
291        let (c1, c2, c3) = <(C1, C2, C3)>::deserialize(d)?;
292        Ok(Self(c1, c2, c3))
293    }
294}
295
296impl<C1: schemars::JsonSchema, C2: schemars::JsonSchema, C3: schemars::JsonSchema>
297    schemars::JsonSchema for Tuple3<C1, C2, C3>
298{
299    fn schema_name() -> ::std::borrow::Cow<'static, str> {
300        format!(
301            "Tuple3<{},{},{}>",
302            C1::schema_name(),
303            C2::schema_name(),
304            C3::schema_name()
305        )
306        .into()
307    }
308    fn json_schema(generator: &mut schemars::SchemaGenerator) -> schemars::Schema {
309        let c1_val = serde_json::to_value(generator.subschema_for::<C1>()).expect("schema");
310        let c2_val = serde_json::to_value(generator.subschema_for::<C2>()).expect("schema");
311        let c3_val = serde_json::to_value(generator.subschema_for::<C3>()).expect("schema");
312        let mut map = serde_json::Map::new();
313        map.insert("type".to_string(), "array".into());
314        map.insert("minItems".to_string(), 3u64.into());
315        map.insert("maxItems".to_string(), 3u64.into());
316        map.insert(
317            "prefixItems".to_string(),
318            serde_json::Value::Array(vec![c1_val, c2_val, c3_val]),
319        );
320        schemars::Schema::from(map)
321    }
322}
323
324impl<C1, C2, C3, C4> serde::Serialize for Tuple4<C1, C2, C3, C4>
325where
326    C1: serde::Serialize,
327    C2: serde::Serialize,
328    C3: serde::Serialize,
329    C4: serde::Serialize,
330{
331    fn serialize<S: serde::Serializer>(&self, s: S) -> Result<S::Ok, S::Error> {
332        (&self.0, &self.1, &self.2, &self.3).serialize(s)
333    }
334}
335
336impl<'de, C1, C2, C3, C4> serde::Deserialize<'de> for Tuple4<C1, C2, C3, C4>
337where
338    C1: serde::Deserialize<'de>,
339    C2: serde::Deserialize<'de>,
340    C3: serde::Deserialize<'de>,
341    C4: serde::Deserialize<'de>,
342{
343    fn deserialize<D: serde::Deserializer<'de>>(d: D) -> Result<Self, D::Error> {
344        let (c1, c2, c3, c4) = <(C1, C2, C3, C4)>::deserialize(d)?;
345        Ok(Self(c1, c2, c3, c4))
346    }
347}
348
349impl<C1, C2, C3, C4> schemars::JsonSchema for Tuple4<C1, C2, C3, C4>
350where
351    C1: schemars::JsonSchema,
352    C2: schemars::JsonSchema,
353    C3: schemars::JsonSchema,
354    C4: schemars::JsonSchema,
355{
356    fn schema_name() -> ::std::borrow::Cow<'static, str> {
357        format!(
358            "Tuple4<{},{},{},{}>",
359            C1::schema_name(),
360            C2::schema_name(),
361            C3::schema_name(),
362            C4::schema_name()
363        )
364        .into()
365    }
366    fn json_schema(generator: &mut schemars::SchemaGenerator) -> schemars::Schema {
367        let c1_val = serde_json::to_value(generator.subschema_for::<C1>()).expect("schema");
368        let c2_val = serde_json::to_value(generator.subschema_for::<C2>()).expect("schema");
369        let c3_val = serde_json::to_value(generator.subschema_for::<C3>()).expect("schema");
370        let c4_val = serde_json::to_value(generator.subschema_for::<C4>()).expect("schema");
371        let mut map = serde_json::Map::new();
372        map.insert("type".to_string(), "array".into());
373        map.insert("minItems".to_string(), 4u64.into());
374        map.insert("maxItems".to_string(), 4u64.into());
375        map.insert(
376            "prefixItems".to_string(),
377            serde_json::Value::Array(vec![c1_val, c2_val, c3_val, c4_val]),
378        );
379        schemars::Schema::from(map)
380    }
381}
382
383// ── ElicitIntrospect impls ────────────────────────────────────────────────────
384
385impl<C1: crate::Elicitation + Send, C2: crate::Elicitation + Send> crate::ElicitIntrospect
386    for Tuple2<C1, C2>
387{
388    fn pattern() -> crate::ElicitationPattern {
389        crate::ElicitationPattern::Primitive
390    }
391    fn metadata() -> crate::TypeMetadata {
392        crate::TypeMetadata {
393            type_name: "Tuple2",
394            description: <Self as crate::Prompt>::prompt(),
395            details: crate::PatternDetails::Primitive,
396        }
397    }
398}
399
400impl<C1: crate::Elicitation + Send, C2: crate::Elicitation + Send, C3: crate::Elicitation + Send>
401    crate::ElicitIntrospect for Tuple3<C1, C2, C3>
402{
403    fn pattern() -> crate::ElicitationPattern {
404        crate::ElicitationPattern::Primitive
405    }
406    fn metadata() -> crate::TypeMetadata {
407        crate::TypeMetadata {
408            type_name: "Tuple3",
409            description: <Self as crate::Prompt>::prompt(),
410            details: crate::PatternDetails::Primitive,
411        }
412    }
413}
414
415impl<C1, C2, C3, C4> crate::ElicitIntrospect for Tuple4<C1, C2, C3, C4>
416where
417    C1: crate::Elicitation + Send,
418    C2: crate::Elicitation + Send,
419    C3: crate::Elicitation + Send,
420    C4: crate::Elicitation + Send,
421{
422    fn pattern() -> crate::ElicitationPattern {
423        crate::ElicitationPattern::Primitive
424    }
425    fn metadata() -> crate::TypeMetadata {
426        crate::TypeMetadata {
427            type_name: "Tuple4",
428            description: <Self as crate::Prompt>::prompt(),
429            details: crate::PatternDetails::Primitive,
430        }
431    }
432}
433
434// ── ToCodeLiteral impls ───────────────────────────────────────────────────────
435
436mod emit_impls {
437    use super::*;
438    use crate::emit_code::ToCodeLiteral;
439    use proc_macro2::TokenStream;
440
441    impl<C1: ToCodeLiteral, C2: ToCodeLiteral> ToCodeLiteral for Tuple2<C1, C2> {
442        fn to_code_literal(&self) -> TokenStream {
443            let first = self.0.to_code_literal();
444            let second = self.1.to_code_literal();
445            quote::quote! { elicitation::Tuple2::new(#first, #second) }
446        }
447    }
448
449    impl<C1: ToCodeLiteral, C2: ToCodeLiteral, C3: ToCodeLiteral> ToCodeLiteral for Tuple3<C1, C2, C3> {
450        fn to_code_literal(&self) -> TokenStream {
451            let first = self.0.to_code_literal();
452            let second = self.1.to_code_literal();
453            let third = self.2.to_code_literal();
454            quote::quote! { elicitation::Tuple3::new(#first, #second, #third) }
455        }
456    }
457
458    impl<C1: ToCodeLiteral, C2: ToCodeLiteral, C3: ToCodeLiteral, C4: ToCodeLiteral> ToCodeLiteral
459        for Tuple4<C1, C2, C3, C4>
460    {
461        fn to_code_literal(&self) -> TokenStream {
462            let first = self.0.to_code_literal();
463            let second = self.1.to_code_literal();
464            let third = self.2.to_code_literal();
465            let fourth = self.3.to_code_literal();
466            quote::quote! { elicitation::Tuple4::new(#first, #second, #third, #fourth) }
467        }
468    }
469}
elicitation/verification/types/tuples.rs

elicitation/verification/types/
tuples.rs
