elicitation 0.11.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
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340

//! Creusot companion file generator for `elicitation generate creusot`.
//!
//! Takes a `VsmDescriptor` (produced by the source scanner) and emits a Rust
//! source file containing Creusot `#[requires]`/`#[ensures]` contracts that
//! replace what `VerifiedStateMachine::vsm_creusot_proof()` produces at build time.
//!
//! The generated file follows a sound architecture:
//! 1. `#![allow(unexpected_cfgs)]` — suppress unknown cfg key warnings
//! 2. `#[cfg(creusot)] use` imports (fixed prelude + type-resolved)
//! 3. `extern_spec!` for `Established::prove/assert` (so cross-crate ZST calls have no false precondition)
//! 4. `#[cfg(creusot)] #[logic] pub fn inv(state) -> bool { <body> }` — invariant
//! 5. `#[cfg(creusot)] #[ensures(result)] pub fn verify_*_prop_creusot()` — marker (no `#[trusted]`)
//! 6. Per-transition: `extern_spec! { ... }` (scoped trusted axiom) + non-trusted wrapper (real VC for Why3)
//!
//! ## Why `extern_spec!` + non-trusted wrapper?
//!
//! `#[trusted]` on a conclusion axiom-farms: Why3 has no VC to discharge and would
//! accept `#[ensures(1 == 2)]` unconditionally.  `extern_spec!` is scoped: it
//! axiomatises a PREMISE (the original transition function's contract).  The
//! non-trusted wrapper then calls through that function, giving Why3 a real VC:
//! "does the wrapper's `#[ensures(inv(&result.0))]` follow from the extern_spec?"
//! Why3 verifies this by unfolding the extern_spec contract — that's the actual proof.

use std::collections::BTreeSet;
use std::path::Path;

use crate::cli::generate::{
    TypeResolver, find_crate_name,
    scanner::{ArgKind, TransitionFn, VsmDescriptor},
};

// ─── Public API ───────────────────────────────────────────────────────────────

/// Generate the shared elicitation extern_specs file for a crate.
///
/// This must be emitted once per crate (not per VSM) because Creusot rejects
/// duplicate `extern_spec!` declarations for the same function within a crate.
/// Callers include this file as `pub mod elicitation_specs;` in the generated `mod.rs`.
pub fn generate_creusot_shared_file() -> String {
    let lines = vec![
        "// AUTO-GENERATED by `elicitation generate creusot` — DO NOT EDIT".to_string(),
        "//".to_string(),
        "// Shared elicitation extern_specs for this crate's Creusot companions.".to_string(),
        "// Regenerate: elicitation generate creusot --crate-path <root>".to_string(),
        "//".to_string(),
        "// These are emitted once per crate to avoid duplicate extern_spec! errors.".to_string(),
        "#![allow(unexpected_cfgs)]".to_string(),
        String::new(),
        "#[cfg(creusot)]".to_string(),
        "use ::creusot_std::prelude::*;".to_string(),
        "#[cfg(creusot)]".to_string(),
        "use elicitation::{Established, Prop, ProvableFrom};".to_string(),
        String::new(),
        emit_established_extern_specs(),
        String::new(),
    ];
    lines.join("\n") + "\n"
}
///
/// `crate_root` is used to discover the crate name via `Cargo.toml`.  The VSM
/// source file is parsed with [`TypeResolver`] to produce precise `use` imports
/// rather than glob wildcards.
///
/// Returns `Err` with an actionable message when a named invariant is present
/// but `creusot_inv_body` could not be resolved.
#[tracing::instrument(skip(vsm, crate_root), fields(machine = %vsm.machine))]
pub fn generate_creusot_file(
    vsm: &VsmDescriptor,
    crate_root: impl AsRef<Path>,
) -> Result<String, String> {
    let machine = &vsm.machine;
    let state_ty = machine.replace("Machine", "State");
    let crate_root = crate_root.as_ref();
    // Derive crate name from the VSM's own source file, not the (possibly workspace)
    // crate_root.  Walking up from the source file finds the crate's own Cargo.toml.
    let vsm_crate_root = vsm.source_file.parent().unwrap_or(crate_root);
    let crate_name = find_crate_name(vsm_crate_root);

    // Resolve invariant — error only when an invariant exists without a body.
    let inv_parts: Option<(&str, &str, &str)> = match &vsm.invariant {
        Some(p) => {
            let fn_name = p.creusot_fn.as_deref().unwrap_or_else(|| p.name.as_str());
            let body = p.creusot_inv_body.as_deref().ok_or_else(|| {
                let hint_fn = p.creusot_fn.as_deref().unwrap_or("creusot_invariant_fn");
                format!(
                    "cannot generate Creusot companion for {machine}: \
                     invariant body for `{hint_fn}` not found\n  \
                     hint: add `creusot_inv_body = \"...\"` to #[prop(...)] on `{name}`,\n  \
                        or define `pub fn {hint_fn}(state: &{state_ty}) -> bool {{ ... }}`\n  \
                           in a file under the scan root (without #[cfg(creusot)] gate)",
                    name = p.name,
                )
            })?;
            Some((fn_name, p.name.as_str(), body))
        }
        None => None,
    };

    // ── Collect the bare type names this file will reference ─────────────────
    let mut needed: BTreeSet<String> = BTreeSet::new();
    TypeResolver::collect_type(&state_ty, &mut needed);
    if let Some((_, consistent_ty, inv_body)) = inv_parts {
        TypeResolver::collect_type(consistent_ty, &mut needed);
        // Also scan the body for constants and other identifiers (e.g. MAX_PLAYER_HANDS).
        TypeResolver::collect_type(inv_body, &mut needed);
    }
    for tfn in &vsm.transition_fns {
        for arg in &tfn.args {
            match &arg.kind {
                ArgKind::State => {}
                ArgKind::Proof { inner } => TypeResolver::collect_type(inner, &mut needed),
                _ => TypeResolver::collect_type(&arg.ty, &mut needed),
            }
        }
    }
    // Import the transition functions themselves, not just their arg types.
    for name in &vsm.transitions {
        needed.insert(name.clone());
    }
    let needs_kani_label = inv_parts
        .map(|(_, _, body)| body.contains("kani_label"))
        .unwrap_or(false);

    // ── Resolve imports ───────────────────────────────────────────────────────
    let resolver = TypeResolver::build(&vsm.source_file, &crate_name);
    let resolved_imports = resolver.grouped_imports(&needed);

    let mut lines: Vec<String> = Vec::new();

    // ── Header ──────────────────────────────────────────────────────────────
    lines.push("// AUTO-GENERATED by `elicitation generate creusot` — DO NOT EDIT".to_string());
    lines.push("//".to_string());
    lines.push(format!("// Creusot companion contracts for {machine}."));
    lines.push("// Regenerate: elicitation generate creusot --crate-path <root>".to_string());
    lines.push("//".to_string());
    lines.push(
        "// All items are gated with #[cfg(creusot)]; invisible to normal Rust builds.".to_string(),
    );
    lines.push(
        "// The `creusot` cfg key is set by the Creusot toolchain, not by cargo.".to_string(),
    );
    lines.push("#![allow(unexpected_cfgs)]".to_string());
    lines.push(String::new());

    // ── Imports ─────────────────────────────────────────────────────────────
    // Fixed: creusot stdlib prelude and elicitation types.
    // Established/Prop/ProvableFrom extern_specs live in elicitation_specs.rs (shared).
    let mut fixed_imports = vec![
        "::creusot_std::prelude::*".to_string(),
        "elicitation::Established".to_string(),
    ];
    if needs_kani_label {
        fixed_imports.push("elicitation::kani_label".to_string());
    }
    for import in &fixed_imports {
        lines.push("#[cfg(creusot)]".to_string());
        lines.push(format!("use {import};"));
    }
    // Type-resolved: precise imports for every user-crate type referenced.
    for import in &resolved_imports {
        lines.push("#[cfg(creusot)]".to_string());
        lines.push(format!("use {import};"));
    }
    lines.push(String::new());

    // ── Logic invariant fn + wrappers ────────────────────────────────────────
    if let Some((inv_fn, consistent_ty, inv_body)) = inv_parts {
        lines.push("#[cfg(creusot)]".to_string());
        lines.push("#[logic]".to_string());
        // If the body already wraps itself in `pearlite! { ... }`, emit verbatim;
        // otherwise wrap it so plain expressions work too.
        let body_expr = if inv_body.trim_start().starts_with("pearlite!") {
            inv_body.to_string()
        } else {
            format!("pearlite! {{ {inv_body} }}")
        };
        // Prefix parameter with `_` when the body doesn't reference it.
        let state_param = if inv_body.contains("state") {
            "state"
        } else {
            "_state"
        };
        lines.push(format!(
            "pub fn {inv_fn}({state_param}: &{state_ty}) -> bool {{\n    {body_expr}\n}}"
        ));
        lines.push(String::new());

        // ── Marker proof fn (non-trusted: body `true` trivially satisfies `#[ensures(result)]`) ──
        let snake = to_snake(consistent_ty);
        lines.push("#[cfg(creusot)]".to_string());
        lines.push("#[requires(true)]".to_string());
        lines.push("#[ensures(result)]".to_string());
        lines.push(format!(
            "pub fn verify_{snake}_prop_creusot() -> bool {{ true }}"
        ));
        lines.push(String::new());

        // ── Per-transition: extern_spec! (trusted premise) + non-trusted wrapper ──
        for name in &vsm.transitions {
            let tf = vsm.transition_fns.iter().find(|tf| &tf.name == name);
            lines.push(emit_creusot_transition(
                name,
                &state_ty,
                consistent_ty,
                inv_fn,
                tf,
            ));
        }
    }

    Ok(lines.join("\n") + "\n")
}

// ─── Emitters ────────────────────────────────────────────────────────────────

/// Emit `extern_spec!` blocks for `Established::prove` and `Established::assert`.
///
/// These ZST constructors are always infallible.  Without extern_specs Creusot
/// inserts `{false} any` at every call site, making every enclosing VC fail.
/// These specs are trusted axioms (premises), not conclusions — their correctness
/// is independently verified by Kani on the source crate.
fn emit_established_extern_specs() -> String {
    [
        "#[cfg(creusot)]",
        "extern_spec! {",
        "    impl<P: Prop> Established<P> {",
        "        #[requires(true)]",
        "        fn prove<C>(_credential: &C) -> Established<P>",
        "        where P: ProvableFrom<C>;",
        "    }",
        "}",
        "",
        "#[cfg(creusot)]",
        "extern_spec! {",
        "    impl<P: Prop> Established<P> {",
        "        #[requires(true)]",
        "        fn assert() -> Established<P>;",
        "    }",
        "}",
    ]
    .join("\n")
}

/// Emit an `extern_spec!` block (trusted premise) followed by a non-trusted
/// call-through wrapper (which Why3 actually verifies as a real VC).
///
/// ## Architecture
///
/// The `extern_spec!` is a scoped trusted axiom: it tells Creusot "assume
/// `fn_name` satisfies this contract."  The non-trusted wrapper then calls
/// `fn_name`, giving Why3 a real VC: "does `fn_name_creusot`'s postcondition
/// follow from the extern_spec?"  Why3 discharges this by unfolding the extern
/// contract — that is the actual proof obligation.
///
/// This is sound because:
/// - The extern_spec axiomatises a PREMISE (cross-crate function).
/// - The wrapper's postcondition is the CONCLUSION Why3 must prove.
/// - Kani independently verifies the premise on the real function body.
fn emit_creusot_transition(
    fn_name: &str,
    state_ty: &str,
    consistent_ty: &str,
    inv_fn: &str,
    tf: Option<&TransitionFn>,
) -> String {
    let (params, call_args) = match tf {
        Some(tf) => (emit_params(tf, state_ty), emit_call_args(tf)),
        None => (
            format!("state: {state_ty}, proof: Established<{consistent_ty}>"),
            "state, proof".to_string(),
        ),
    };
    let ret = format!("({state_ty}, Established<{consistent_ty}>)");

    let mut lines: Vec<String> = Vec::new();

    // extern_spec!: scoped trusted axiom (premise)
    lines.push("#[cfg(creusot)]".to_string());
    lines.push("extern_spec! {".to_string());
    lines.push(format!("    #[requires({inv_fn}(&state))]"));
    lines.push(format!("    #[ensures({inv_fn}(&result.0))]"));
    lines.push(format!("    fn {fn_name}({params}) -> {ret};"));
    lines.push("}".to_string());
    lines.push(String::new());

    // Non-trusted wrapper: real VC for Why3 (conclusion)
    lines.push("#[cfg(creusot)]".to_string());
    lines.push(format!("#[requires({inv_fn}(&state))]"));
    lines.push(format!("#[ensures({inv_fn}(&result.0))]"));
    // `pub` (not `pub(crate)`) avoids spurious `dead_code` warnings under
    // Creusot's compiler, where these functions serve as proof obligations
    // but have no regular Rust call sites.
    lines.push(format!(
        "pub fn {fn_name}_creusot({params}) -> {ret} {{ {fn_name}({call_args}) }}"
    ));
    lines.push(String::new());

    lines.join("\n")
}

/// Emit function parameter list: `state: State, proof: Established<T>, extra: Type, ...`
fn emit_params(tf: &TransitionFn, state_ty: &str) -> String {
    let mut parts: Vec<String> = Vec::new();
    for arg in &tf.args {
        let (name, ty) = match &arg.kind {
            ArgKind::State => ("state".to_string(), state_ty.to_string()),
            ArgKind::Proof { inner } => (arg.name.clone(), format!("Established<{inner}>")),
            _ => (arg.name.trim_start_matches('_').to_string(), arg.ty.clone()),
        };
        parts.push(format!("{name}: {ty}"));
    }
    parts.join(", ")
}

/// Emit call argument list: `state, proof, extra, ...`
fn emit_call_args(tf: &TransitionFn) -> String {
    tf.args
        .iter()
        .map(|arg| match arg.kind {
            ArgKind::State => "state".to_string(),
            ArgKind::Proof { .. } => arg.name.clone(),
            _ => arg.name.trim_start_matches('_').to_string(),
        })
        .collect::<Vec<_>>()
        .join(", ")
}

// ─── Helpers ─────────────────────────────────────────────────────────────────

/// Convert PascalCase to snake_case.
fn to_snake(s: &str) -> String {
    let mut out = String::new();
    for (i, ch) in s.chars().enumerate() {
        if ch.is_uppercase() && i > 0 {
            out.push('_');
        }
        out.push(ch.to_ascii_lowercase());
    }
    out
}