elicitation 0.10.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
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154

//! [`Elicitation`] implementations for [`std::sync::atomic`] types.
//!
//! All eleven non-pointer atomic types are supported:
//! [`AtomicBool`], [`AtomicI8`], [`AtomicI16`], [`AtomicI32`], [`AtomicI64`],
//! [`AtomicIsize`], [`AtomicU8`], [`AtomicU16`], [`AtomicU32`], [`AtomicU64`],
//! and [`AtomicUsize`].
//!
//! Each atomic wraps its corresponding primitive: eliciting an atomic value
//! elicits the underlying primitive and wraps it with `Atomic*::new(val)`.
//!
//! The proof methods generate harnesses that verify the core atomic invariant:
//! `Atomic*::new(val).load(SeqCst) == val`. Verus and Creusot proofs are
//! `#[trusted]` since those tools cannot verify unsafe hardware atomic ops.
//!
//! [`ToCodeLiteral`](crate::emit_code::ToCodeLiteral) is implemented in
//! `emit_code.rs` alongside the other primitive impls.

use std::sync::atomic::{
    AtomicBool, AtomicI8, AtomicI16, AtomicI32, AtomicI64, AtomicIsize, AtomicU8, AtomicU16,
    AtomicU32, AtomicU64, AtomicUsize,
};

use crate::{
    ElicitCommunicator, ElicitIntrospect, ElicitResult, Elicitation, ElicitationPattern,
    PatternDetails, Prompt, TypeMetadata,
};

macro_rules! impl_atomic_elicitation {
    (bool: $atomic:ty, $atomic_path:literal) => {
        impl Prompt for $atomic {
            fn prompt() -> Option<&'static str> {
                Some(concat!(
                    "Please enter a boolean value for ",
                    stringify!($atomic),
                    " (true or false):"
                ))
            }
        }

        impl Elicitation for $atomic {
            type Style = <bool as Elicitation>::Style;

            #[tracing::instrument(skip(communicator), fields(type_name = stringify!($atomic)))]
            async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
                tracing::debug!(concat!("Eliciting ", stringify!($atomic), " via bool"));
                let val = bool::elicit(communicator).await?;
                Ok(<$atomic>::new(val))
            }

            fn kani_proof() -> proc_macro2::TokenStream {
                let mut ts = crate::verification::proof_helpers::kani_atomic($atomic_path, "bool");
                ts.extend(<bool as Elicitation>::kani_proof());
                ts
            }

            fn verus_proof() -> proc_macro2::TokenStream {
                crate::verification::proof_helpers::verus_atomic($atomic_path, "bool")
            }

            fn creusot_proof() -> proc_macro2::TokenStream {
                crate::verification::proof_helpers::creusot_atomic($atomic_path, "bool")
            }
        }

        impl ElicitIntrospect for $atomic {
            fn pattern() -> ElicitationPattern {
                ElicitationPattern::Affirm
            }

            fn metadata() -> TypeMetadata {
                TypeMetadata {
                    type_name: stringify!($atomic),
                    description: <Self as Prompt>::prompt(),
                    details: PatternDetails::Affirm,
                }
            }
        }
    };

    (int: $atomic:ty, $atomic_path:literal => $prim:ty) => {
        impl Prompt for $atomic {
            fn prompt() -> Option<&'static str> {
                Some(concat!(
                    "Please enter a ",
                    stringify!($prim),
                    " value for ",
                    stringify!($atomic),
                    ":"
                ))
            }
        }

        impl Elicitation for $atomic {
            type Style = <$prim as Elicitation>::Style;

            #[tracing::instrument(skip(communicator), fields(type_name = stringify!($atomic)))]
            async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
                tracing::debug!(concat!(
                    "Eliciting ",
                    stringify!($atomic),
                    " via ",
                    stringify!($prim)
                ));
                let val = <$prim as Elicitation>::elicit(communicator).await?;
                Ok(<$atomic>::new(val))
            }

            fn kani_proof() -> proc_macro2::TokenStream {
                let mut ts = crate::verification::proof_helpers::kani_atomic(
                    $atomic_path,
                    stringify!($prim),
                );
                ts.extend(<$prim as Elicitation>::kani_proof());
                ts
            }

            fn verus_proof() -> proc_macro2::TokenStream {
                crate::verification::proof_helpers::verus_atomic($atomic_path, stringify!($prim))
            }

            fn creusot_proof() -> proc_macro2::TokenStream {
                crate::verification::proof_helpers::creusot_atomic($atomic_path, stringify!($prim))
            }
        }

        impl ElicitIntrospect for $atomic {
            fn pattern() -> ElicitationPattern {
                ElicitationPattern::Primitive
            }

            fn metadata() -> TypeMetadata {
                TypeMetadata {
                    type_name: stringify!($atomic),
                    description: <Self as Prompt>::prompt(),
                    details: PatternDetails::Primitive,
                }
            }
        }
    };
}

impl_atomic_elicitation!(bool: AtomicBool, "::std::sync::atomic::AtomicBool");

impl_atomic_elicitation!(int: AtomicI8,    "::std::sync::atomic::AtomicI8"    => i8);
impl_atomic_elicitation!(int: AtomicI16,   "::std::sync::atomic::AtomicI16"   => i16);
impl_atomic_elicitation!(int: AtomicI32,   "::std::sync::atomic::AtomicI32"   => i32);
impl_atomic_elicitation!(int: AtomicI64,   "::std::sync::atomic::AtomicI64"   => i64);
impl_atomic_elicitation!(int: AtomicIsize, "::std::sync::atomic::AtomicIsize" => isize);

impl_atomic_elicitation!(int: AtomicU8,    "::std::sync::atomic::AtomicU8"    => u8);
impl_atomic_elicitation!(int: AtomicU16,   "::std::sync::atomic::AtomicU16"   => u16);
impl_atomic_elicitation!(int: AtomicU32,   "::std::sync::atomic::AtomicU32"   => u32);
impl_atomic_elicitation!(int: AtomicU64,   "::std::sync::atomic::AtomicU64"   => u64);
impl_atomic_elicitation!(int: AtomicUsize, "::std::sync::atomic::AtomicUsize" => usize);