elicitation 0.11.1

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

//! Tests for [`FormalMethod`] and the blanket impl.
//!
//! Verifies that:
//! - Any `Fn(In, Established<PIn>) -> (Out, Established<POut>)` satisfies
//!   `FormalMethod` automatically.
//! - Proof tokens flow correctly through composition.
//! - Zero-cost: `Established` tokens contribute no runtime size.

use elicitation::{Established, FormalMethod, Prop, contracts::ProvableFrom};

// ── Propositions used in tests ────────────────────────────────────────────────

#[derive(Prop)]
struct Validated;

#[derive(Prop)]
struct Normalised;

#[derive(Prop)]
struct Stored;

// ── Helper: a credential that mints Validated ─────────────────────────────────

struct ValidInput;
impl ProvableFrom<ValidInput> for Validated {}

// ── Tests ─────────────────────────────────────────────────────────────────────

#[test]
fn plain_fn_satisfies_formal_method_bound() {
    fn normalise(s: String, _proof: Established<Validated>) -> (String, Established<Normalised>) {
        (s.trim().to_lowercase(), Established::assert())
    }

    // The bound check: normalise must implement FormalMethod<…>
    fn assert_formal<F: FormalMethod<String, Validated, String, Normalised>>(_f: &F) {}
    assert_formal(&normalise);
}

#[test]
fn closure_satisfies_formal_method_bound() {
    let normalise =
        |s: String, _proof: Established<Validated>| -> (String, Established<Normalised>) {
            (s.to_uppercase(), Established::assert())
        };

    fn assert_formal<F: FormalMethod<String, Validated, String, Normalised>>(_f: &F) {}
    assert_formal(&normalise);
}

#[test]
fn call_formal_produces_correct_output() {
    fn process(n: u32, _proof: Established<Validated>) -> (u32, Established<Normalised>) {
        (n * 2, Established::assert())
    }

    let proof_in = Established::<Validated>::prove(&ValidInput);
    let (result, _proof_out) = process.call_formal(21, proof_in);
    assert_eq!(result, 42);
}

#[test]
fn formal_methods_compose_proof_flows_through() {
    // Step 1: Validated → Normalised
    fn normalise(s: String, _proof: Established<Validated>) -> (String, Established<Normalised>) {
        (s.trim().to_string(), Established::assert())
    }

    // Step 2: Normalised → Stored
    fn store(s: String, _proof: Established<Normalised>) -> (usize, Established<Stored>) {
        (s.len(), Established::assert())
    }

    let validated = Established::<Validated>::prove(&ValidInput);
    let (normalised_val, normalised_proof) =
        normalise.call_formal("  hello  ".to_string(), validated);
    let (len, _stored_proof) = store.call_formal(normalised_val, normalised_proof);

    assert_eq!(len, 5);
}

#[test]
fn proof_tokens_are_zero_sized() {
    let p = Established::<Validated>::assert();
    assert_eq!(std::mem::size_of_val(&p), 0);

    let q = Established::<Normalised>::assert();
    assert_eq!(std::mem::size_of_val(&q), 0);
}

#[test]
fn harness_defaults_return_empty_token_stream() {
    type F = fn(String, Established<Validated>) -> (String, Established<Normalised>);
    // Default harness methods return empty streams — no panic expected.
    let _ = <F as FormalMethod<String, Validated, String, Normalised>>::kani_harness();
    let _ = <F as FormalMethod<String, Validated, String, Normalised>>::verus_harness();
    let _ = <F as FormalMethod<String, Validated, String, Normalised>>::creusot_harness();
}