elicitation/
rand_rng.rs

1//! Random number generator elicitation.
2//!
3//! Available with the `rand` feature.
4//!
5//! This module provides `Elicitation` implementations for common RNG types
6//! from the `rand` ecosystem, allowing agents to conversationally construct
7//! random number generators with specific seeds.
8//!
9//! # Example
10//!
11//! ```rust,ignore
12//! use elicitation::Elicitation;
13//! use rand::rngs::StdRng;
14//! use rand::Rng;
15//!
16//! async fn example(communicator: &impl ElicitCommunicator) {
17//!     // Agent elicits seed for reproducibility
18//!     let rng = StdRng::elicit(communicator).await?;
19//!     
20//!     // Use RNG
21//!     let value: u32 = rng.gen();
22//! }
23//! ```
24
25use crate::{ElicitCommunicator, ElicitResult, Elicitation, Prompt, default_style};
26use rand::SeedableRng;
27use rand::rngs::StdRng;
28use rand_chacha::ChaCha8Rng;
29
30// Style types for RNG elicitation
31default_style!(StdRng => StdRngStyle);
32default_style!(ChaCha8Rng => ChaCha8RngStyle);
33
34// ============================================================================
35// StdRng - Standard, reproducible RNG
36// ============================================================================
37
38impl Prompt for StdRng {
39    fn prompt() -> Option<&'static str> {
40        Some("Enter seed for standard RNG (u64):")
41    }
42}
43
44impl Elicitation for StdRng {
45    type Style = StdRngStyle;
46
47    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
48        // Elicit seed from agent
49        let seed: u64 = u64::elicit(communicator).await?;
50
51        // Construct RNG (trust rand's implementation)
52        Ok(StdRng::seed_from_u64(seed))
53    }
54
55    fn kani_proof() -> proc_macro2::TokenStream {
56        proc_macro2::TokenStream::new()
57    }
58
59    fn verus_proof() -> proc_macro2::TokenStream {
60        proc_macro2::TokenStream::new()
61    }
62
63    fn creusot_proof() -> proc_macro2::TokenStream {
64        proc_macro2::TokenStream::new()
65    }
66}
67
68// ============================================================================
69// ChaCha8Rng - Cryptographically secure RNG
70// ============================================================================
71
72impl Prompt for ChaCha8Rng {
73    fn prompt() -> Option<&'static str> {
74        Some("Enter seed for cryptographic RNG (u64):")
75    }
76}
77
78impl Elicitation for ChaCha8Rng {
79    type Style = ChaCha8RngStyle;
80
81    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
82        let seed: u64 = u64::elicit(communicator).await?;
83        Ok(ChaCha8Rng::seed_from_u64(seed))
84    }
85
86    fn kani_proof() -> proc_macro2::TokenStream {
87        proc_macro2::TokenStream::new()
88    }
89
90    fn verus_proof() -> proc_macro2::TokenStream {
91        proc_macro2::TokenStream::new()
92    }
93
94    fn creusot_proof() -> proc_macro2::TokenStream {
95        proc_macro2::TokenStream::new()
96    }
97}
elicitation/rand_rng.rs

elicitation/
rand_rng.rs
