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
//! Random number generator elicitation.
//!
//! Available with the `rand` feature.
//!
//! This module provides `Elicitation` implementations for common RNG types
//! from the `rand` ecosystem, allowing agents to conversationally construct
//! random number generators with specific seeds.
//!
//! # Example
//!
//! ```rust,ignore
//! use elicitation::Elicitation;
//! use rand::rngs::StdRng;
//! use rand::Rng;
//!
//! async fn example(communicator: &impl ElicitCommunicator) {
//! // Agent elicits seed for reproducibility
//! let rng = StdRng::elicit(communicator).await?;
//!
//! // Use RNG
//! let value: u32 = rng.gen();
//! }
//! ```
use crate::{ElicitCommunicator, ElicitResult, Elicitation, Prompt, default_style};
use rand::SeedableRng;
use rand::rngs::StdRng;
use rand_chacha::ChaCha8Rng;
// Style types for RNG elicitation
default_style!(StdRng => StdRngStyle);
default_style!(ChaCha8Rng => ChaCha8RngStyle);
// ============================================================================
// StdRng - Standard, reproducible RNG
// ============================================================================
impl Prompt for StdRng {
fn prompt() -> Option<&'static str> {
Some("Enter seed for standard RNG (u64):")
}
}
impl Elicitation for StdRng {
type Style = StdRngStyle;
async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
// Elicit seed from agent
let seed: u64 = u64::elicit(communicator).await?;
// Construct RNG (trust rand's implementation)
Ok(StdRng::seed_from_u64(seed))
}
fn kani_proof() -> proc_macro2::TokenStream {
proc_macro2::TokenStream::new()
}
fn verus_proof() -> proc_macro2::TokenStream {
proc_macro2::TokenStream::new()
}
fn creusot_proof() -> proc_macro2::TokenStream {
proc_macro2::TokenStream::new()
}
}
// ============================================================================
// ChaCha8Rng - Cryptographically secure RNG
// ============================================================================
impl Prompt for ChaCha8Rng {
fn prompt() -> Option<&'static str> {
Some("Enter seed for cryptographic RNG (u64):")
}
}
impl Elicitation for ChaCha8Rng {
type Style = ChaCha8RngStyle;
async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
let seed: u64 = u64::elicit(communicator).await?;
Ok(ChaCha8Rng::seed_from_u64(seed))
}
fn kani_proof() -> proc_macro2::TokenStream {
proc_macro2::TokenStream::new()
}
fn verus_proof() -> proc_macro2::TokenStream {
proc_macro2::TokenStream::new()
}
fn creusot_proof() -> proc_macro2::TokenStream {
proc_macro2::TokenStream::new()
}
}