elicitation 0.8.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

//! Command-line interface for elicitation tools.
//!
//! Provides verification orchestration, analysis, and utilities.

use clap::{Parser, Subcommand};
use derive_getters::Getters;
use std::path::PathBuf;

/// Elicitation library tools and verification
#[derive(Debug, Clone, Parser, Getters)]
#[command(name = "elicitation")]
#[command(about = "Type-safe LLM elicitation with formal verification")]
pub struct Cli {
    /// The command to execute
    #[command(subcommand)]
    command: Commands,
}

/// Available commands
#[derive(Debug, Clone, Subcommand)]
pub enum Commands {
    /// Run and manage Kani verification proofs
    Verify {
        /// Action to perform
        #[command(subcommand)]
        action: VerifyAction,
    },

    /// Run and manage Prusti verification proofs
    Prusti {
        /// Action to perform
        #[command(subcommand)]
        action: PrustiAction,
    },
}

/// Verification actions
#[derive(Debug, Clone, Subcommand)]
pub enum VerifyAction {
    /// List all proof harnesses
    List,

    /// Run all proofs with CSV tracking
    Run {
        /// CSV output file
        #[arg(short, long, default_value = "kani_verification_results.csv")]
        output: PathBuf,

        /// Timeout per test in seconds
        #[arg(short, long, default_value_t = 300)]
        timeout: u64,

        /// Resume mode: skip already-passed tests
        #[arg(short, long)]
        resume: bool,
    },

    /// Show summary statistics from CSV
    Summary {
        /// CSV file to analyze
        #[arg(default_value = "kani_verification_results.csv")]
        file: PathBuf,
    },

    /// Show failed tests from CSV
    Failed {
        /// CSV file to analyze
        #[arg(default_value = "kani_verification_results.csv")]
        file: PathBuf,
    },
}

/// Prusti verification actions
#[derive(Debug, Clone, Subcommand)]
pub enum PrustiAction {
    /// List all proof modules
    List,

    /// Run Prusti verification with CSV tracking
    Run {
        /// CSV output file
        #[arg(short, long, default_value = "prusti_verification_results.csv")]
        output: PathBuf,

        /// Timeout in seconds
        #[arg(short, long, default_value_t = 600)]
        timeout: u64,
    },

    /// Show summary statistics from CSV
    Summary {
        /// CSV file to analyze
        #[arg(short, long, default_value = "prusti_verification_results.csv")]
        file: PathBuf,
    },

    /// Show failed modules from CSV
    Failed {
        /// CSV file to analyze
        #[arg(short, long, default_value = "prusti_verification_results.csv")]
        file: PathBuf,
    },
}

/// Execute the CLI command.
#[tracing::instrument(skip(cli))]
pub fn execute(cli: Cli) -> anyhow::Result<()> {
    tracing::debug!("Executing CLI command");

    match cli.command() {
        Commands::Verify { action } => crate::verification::runner::handle(action),
        Commands::Prusti { action } => handle_prusti(action),
    }
}

/// Handle Prusti verification commands.
#[tracing::instrument(skip(action))]
fn handle_prusti(action: &PrustiAction) -> anyhow::Result<()> {
    tracing::debug!(action = ?action, "Handling Prusti command");

    match action {
        PrustiAction::List => crate::verification::prusti_runner::list_modules(),
        PrustiAction::Run { output, timeout } => {
            crate::verification::prusti_runner::run_all(output, *timeout)
        }
        PrustiAction::Summary { file } => crate::verification::prusti_runner::show_summary(file),
        PrustiAction::Failed { file } => crate::verification::prusti_runner::show_failed(file),
    }
}