elicitation/containers/
array.rs

1//! Fixed-size array [T; N] implementation using const generics.
2
3use crate::{ElicitCommunicator, ElicitResult, Elicitation, Prompt};
4
5// Default-only style for arrays
6#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Default)]
7pub enum ArrayStyle {
8    #[default]
9    Default,
10}
11
12impl Prompt for ArrayStyle {
13    fn prompt() -> Option<&'static str> {
14        None
15    }
16}
17
18impl Elicitation for ArrayStyle {
19    type Style = ArrayStyle;
20
21    #[tracing::instrument(skip(_communicator), level = "trace")]
22    async fn elicit<C: ElicitCommunicator>(_communicator: &C) -> ElicitResult<Self> {
23        Ok(Self::Default)
24    }
25
26    fn kani_proof() -> proc_macro2::TokenStream {
27        crate::verification::proof_helpers::kani_single_variant_enum("ArrayStyle")
28    }
29
30    fn verus_proof() -> proc_macro2::TokenStream {
31        crate::verification::proof_helpers::verus_single_variant_enum("ArrayStyle")
32    }
33
34    fn creusot_proof() -> proc_macro2::TokenStream {
35        crate::verification::proof_helpers::creusot_single_variant_enum("ArrayStyle")
36    }
37}
38
39impl crate::style::ElicitationStyle for ArrayStyle {}
40
41impl<T, const N: usize> Prompt for [T; N]
42where
43    T: Elicitation + Send,
44{
45    fn prompt() -> Option<&'static str> {
46        Some("Eliciting fixed-size array elements:")
47    }
48}
49
50impl<T, const N: usize> Elicitation for [T; N]
51where
52    T: Elicitation + Send,
53{
54    type Style = ArrayStyle;
55
56    #[tracing::instrument(skip(communicator), fields(
57        item_type = std::any::type_name::<T>(),
58        size = N
59    ))]
60    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
61        tracing::debug!(size = N, "Eliciting fixed-size array");
62
63        // Collect items into a Vec first
64        let mut items = Vec::with_capacity(N);
65
66        for i in 0..N {
67            tracing::debug!(index = i, total = N, "Eliciting array element");
68            let item = T::elicit(communicator).await?;
69            items.push(item);
70        }
71
72        // Convert Vec to array using try_into
73        items.try_into().map_err(|_| {
74            // This should never happen since we pre-allocated N items
75            crate::ElicitError::new(crate::ElicitErrorKind::InvalidFormat {
76                expected: format!("array of size {}", N),
77                received: "incorrect size".to_string(),
78            })
79        })
80    }
81
82    fn kani_proof() -> proc_macro2::TokenStream {
83        <T as Elicitation>::kani_proof()
84    }
85
86    fn verus_proof() -> proc_macro2::TokenStream {
87        <T as Elicitation>::verus_proof()
88    }
89
90    fn creusot_proof() -> proc_macro2::TokenStream {
91        <T as Elicitation>::creusot_proof()
92    }
93}
elicitation/containers/array.rs

elicitation/containers/
array.rs
