elicitation 0.10.0

//! Tuple type implementations using macros.

#![allow(non_snake_case)]

use crate::{ElicitCommunicator, ElicitResult, Elicitation, Prompt};

/// Macro to implement Elicitation for tuples up to arity 12.
macro_rules! impl_tuple_elicit {
    // Base case: empty tuple (unit type is already handled by primitives)

    // Single element and up
    ($($T:ident $idx:tt),+) => {
        // Each tuple size gets its own default-only style enum
        paste::paste! {
            #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Default)]
            pub enum [<Tuple $( $idx )+ Style>] {
                #[default]
                Default,
            }

            impl Prompt for [<Tuple $( $idx )+ Style>] {
                fn prompt() -> Option<&'static str> {
                    None
                }
            }

            impl Elicitation for [<Tuple $( $idx )+ Style>] {
                type Style = [<Tuple $( $idx )+ Style>];

                #[tracing::instrument(skip(_communicator), level = "trace")]
                async fn elicit<C: ElicitCommunicator>(_communicator: &C) -> ElicitResult<Self> {
                    Ok(Self::Default)
                }

    fn kani_proof() -> proc_macro2::TokenStream {
        // paste!-generated name; derive at runtime via type_name
        let short = std::any::type_name::<Self>()
            .split("::")
            .last()
            .unwrap_or("TupleStyle");
        crate::verification::proof_helpers::kani_single_variant_enum(short)
    }

    fn verus_proof() -> proc_macro2::TokenStream {
        let short = std::any::type_name::<Self>()
            .split("::")
            .last()
            .unwrap_or("TupleStyle");
        crate::verification::proof_helpers::verus_single_variant_enum(short)
    }

    fn creusot_proof() -> proc_macro2::TokenStream {
        let short = std::any::type_name::<Self>()
            .split("::")
            .last()
            .unwrap_or("TupleStyle");
        crate::verification::proof_helpers::creusot_single_variant_enum(short)
    }
}

            impl crate::style::ElicitationStyle for [<Tuple $( $idx )+ Style>] {}
        }

        impl<$($T),+> Prompt for ($($T,)+)
        where
            $($T: Elicitation + Send,)+
        {
            fn prompt() -> Option<&'static str> {
                Some("Eliciting tuple elements:")
            }
        }

        impl<$($T),+> Elicitation for ($($T,)+)
        where
            $($T: Elicitation + Send,)+
        {
            paste::paste! {
                type Style = [<Tuple $( $idx )+ Style>];
            }

            #[tracing::instrument(skip(communicator), fields(
                tuple_size = count!($($T)+),
                types = concat!($(stringify!($T), ", "),+)
            ))]
            async fn elicit<C: ElicitCommunicator>(
                communicator: &C,
            ) -> ElicitResult<Self> {
                tracing::debug!("Eliciting tuple");

                $(
                    tracing::debug!(index = $idx, type_name = std::any::type_name::<$T>(), "Eliciting tuple element");
                    let $T = $T::elicit(communicator).await?;
                )+

                tracing::debug!("Tuple complete");
                Ok(($($T,)+))
            }

    fn kani_proof() -> proc_macro2::TokenStream {
        // Compose all element proofs: proof(T1,T2,...) = proof(T1) + proof(T2) + ...
        let mut ts = proc_macro2::TokenStream::new();
        $(ts.extend(<$T as Elicitation>::kani_proof());)+
        ts
    }

    fn verus_proof() -> proc_macro2::TokenStream {
        let mut ts = proc_macro2::TokenStream::new();
        $(ts.extend(<$T as Elicitation>::verus_proof());)+
        ts
    }

    fn creusot_proof() -> proc_macro2::TokenStream {
        let mut ts = proc_macro2::TokenStream::new();
        $(ts.extend(<$T as Elicitation>::creusot_proof());)+
        ts
    }
}
    };
}

/// Helper macro to count the number of items
macro_rules! count {
    () => (0);
    ($head:tt $($tail:tt)*) => (1 + count!($($tail)*));
}

// Unit type () - the 0-tuple
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Default)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum UnitStyle {
    #[default]
    Default,
}

impl Prompt for UnitStyle {
    fn prompt() -> Option<&'static str> {
        None
    }
}

impl Elicitation for UnitStyle {
    type Style = UnitStyle;

    #[tracing::instrument(skip(_communicator), level = "trace")]
    async fn elicit<C: ElicitCommunicator>(_communicator: &C) -> ElicitResult<Self> {
        Ok(Self::Default)
    }

    fn kani_proof() -> proc_macro2::TokenStream {
        crate::verification::proof_helpers::kani_single_variant_enum("UnitStyle")
    }

    fn verus_proof() -> proc_macro2::TokenStream {
        crate::verification::proof_helpers::verus_single_variant_enum("UnitStyle")
    }

    fn creusot_proof() -> proc_macro2::TokenStream {
        crate::verification::proof_helpers::creusot_single_variant_enum("UnitStyle")
    }
}

impl crate::style::ElicitationStyle for UnitStyle {}

impl Prompt for () {
    fn prompt() -> Option<&'static str> {
        None
    }
}

impl Elicitation for () {
    type Style = UnitStyle;

    #[tracing::instrument(skip(_communicator), level = "trace")]
    async fn elicit<C: ElicitCommunicator>(_communicator: &C) -> ElicitResult<Self> {
        tracing::debug!("Eliciting unit type ()");
        Ok(())
    }

    fn kani_proof() -> proc_macro2::TokenStream {
        crate::verification::proof_helpers::kani_unit_struct("UnitTuple")
    }

    fn verus_proof() -> proc_macro2::TokenStream {
        crate::verification::proof_helpers::verus_unit_struct("UnitTuple")
    }

    fn creusot_proof() -> proc_macro2::TokenStream {
        crate::verification::proof_helpers::creusot_unit_struct("UnitTuple")
    }
}

// Implement for tuples of arity 1 through 12
impl_tuple_elicit!(T0 0);
impl_tuple_elicit!(T0 0, T1 1);
impl_tuple_elicit!(T0 0, T1 1, T2 2);
impl_tuple_elicit!(T0 0, T1 1, T2 2, T3 3);
impl_tuple_elicit!(T0 0, T1 1, T2 2, T3 3, T4 4);
impl_tuple_elicit!(T0 0, T1 1, T2 2, T3 3, T4 4, T5 5);
impl_tuple_elicit!(T0 0, T1 1, T2 2, T3 3, T4 4, T5 5, T6 6);
impl_tuple_elicit!(T0 0, T1 1, T2 2, T3 3, T4 4, T5 5, T6 6, T7 7);
impl_tuple_elicit!(T0 0, T1 1, T2 2, T3 3, T4 4, T5 5, T6 6, T7 7, T8 8);
impl_tuple_elicit!(T0 0, T1 1, T2 2, T3 3, T4 4, T5 5, T6 6, T7 7, T8 8, T9 9);
impl_tuple_elicit!(T0 0, T1 1, T2 2, T3 3, T4 4, T5 5, T6 6, T7 7, T8 8, T9 9, T10 10);
impl_tuple_elicit!(T0 0, T1 1, T2 2, T3 3, T4 4, T5 5, T6 6, T7 7, T8 8, T9 9, T10 10, T11 11);