v0.8.0 - Filter Trait for Filtered Selection

elicitation v0.8.0 - Introspection, Verification, and Filtering

⚠️ Breaking Changes

This is a major release with breaking API changes to the Select and Survey traits.

API Changes

• Select::options() now returns Vec<Self> instead of &'static [Self]
• Select::labels() now returns Vec<String> instead of Vec<&'static str>
• Survey::fields() now returns Vec<FieldInfo> instead of &'static [FieldInfo]
• ElicitCommunicator::elicitation_context() method added to trait

Migration: If you have custom implementations of Select or Survey, update your return types from static slices to owned Vec types. Most users relying on derive macros will see no impact.

✨ Major Features

🔍 Introspection & Observability

New ElicitIntrospect trait provides compile-time metadata about elicitation patterns:

use elicitation::{ElicitIntrospect, ElicitationPattern, PatternDetails};

// Get metadata for any Elicitation type
let meta = MyType::metadata();
println!("Type: {}", meta.type_name);
println!("Pattern: {}", meta.pattern().as_str()); // "Select", "Survey", "Affirm"

// Inspect Survey fields before elicitation
if let PatternDetails::Survey { fields } = meta.details {
    for field in fields {
        println!("Field: {} ({})", field.name, field.type_name);
    }
}

Key capabilities:

• Zero-runtime-cost metadata via ElicitIntrospect::metadata()
• Pattern introspection: Select, Survey, Affirm, or Direct
• Field enumeration for Survey types
• Integration with tracing and metrics

Context Tracking:

// Track nested elicitation chains
let context = communicator.elicitation_context();
if let Some(meta) = context.current_type()? {
    tracing::info!(
        type_name = %meta.type_name,
        pattern = %meta.pattern().as_str(),
        "Currently eliciting"
    );
}

🔬 Formal Verification with Kani

New Elicitation::kani_proof() method enables compositional verification:

impl Elicitation for Config {
    #[cfg(kani)]
    fn kani_proof() {
        // Verify all fields compositionally
        I8Positive::kani_proof();  // Field 1 verified
        U8NonZero::kani_proof();   // Field 2 verified
        // Tautological: all parts verified ⟹ whole verified
        assert!(true, "Compositional verification");
    }
}

Verification Legos Pattern:

• Manual proofs for primitives (I8Positive, U8NonZero, etc.)
• Compositional proofs for structs (auto-generated by derive macro)
• Zero runtime overhead (compiled away in release builds)
• See FORMAL_VERIFICATION_LEGOS.md for full methodology

🎯 Filter Trait for Filtered Selection

Runtime predicate-based filtering of selection options:

use elicitation::{Select, Filter};

// Filter enum variants with a closure
let warm_colors = Color::select_with_filter(|c| {
    matches!(c, Color::Red | Color::Yellow | Color::Orange)
});

// Filter to occupied positions (e.g., for game boards)
let occupied = Position::select_with_filter(Position::is_occupied);

Key capabilities:

• Filter::select_filtered(filter) - Core filtering method
• Select::select_with_filter(filter) - Convenience method with blanket impl
• Works seamlessly with closures via blanket implementation
• Type-safe and composable

📦 ChoiceSet for Dynamic Choices

New ChoiceSet<T> type for runtime-generated option lists:

use elicitation::ChoiceSet;

// Filter at construction
let evens = ChoiceSet::filtered(numbers, |n| n % 2 == 0);

// Chain filters
let filtered = ChoiceSet::new(numbers)
    .with_filter(|n| n % 2 == 0)  // Even numbers
    .with_filter(|n| *n > 5)       // Greater than 5
    .with_prompt("Pick a number:")
    .elicit(&client)
    .await?;

📚 New Examples

• observability_introspection.rs - ElicitIntrospect, metadata, context tracking, tracing integration
• compositional_verification.rs - Layered verification with kani_proof(), proof chains
• dynamic_choices.rs - ChoiceSet usage, runtime filtering, dynamic options

📖 New Documentation

• FORMAL_VERIFICATION_LEGOS.md - Comprehensive compositional verification guide
• Updated examples README with new patterns
• Introspection API documentation

🧪 Testing

• 6 new tests for Filter trait functionality
• 9 new tests for ChoiceSet filtering operations
• All workspace tests passing

🔧 Fixes

• Fixed changelog-update recipe to properly regenerate CHANGELOG.md
• Fixed pre-release recipe to run dry-run (removed --execute flag)
• Fixed feature-gated code for new API signatures
• Added #[allow(dead_code)] to example types

---

Full Changelog: v0.7.0...v0.8.0