elicitation 0.10.0

//! The [`ElicitComplete`] supertrait — the compiler-enforced contract for
//! fully-implemented elicitation support.
//!
//! # Overview
//!
//! [`ElicitComplete`] is a **marker supertrait** that serves as the final gate
//! before a type can be used as a first-class building block in the elicitation
//! framework. It does not add any new runtime behaviour — instead it aggregates
//! every obligation a type must satisfy and lets the compiler enforce all of them
//! in one place.
//!
//! Think of it as a living checklist: when you write `impl ElicitComplete for
//! MyType {}`, the compiler either accepts it (every box is ticked) or rejects it
//! with an error that points directly at what is still missing.
//!
//! # The Supertrait Checklist
//!
//! | Supertrait | What it provides | How it is satisfied |
//! |---|---|---|
//! | [`Elicitation`] | Interactive elicitation + **proof methods** | `#[derive(Elicit)]` or manual impl |
//! | [`ElicitIntrospect`] | Structural metadata (field names, pattern) | Auto-derived by `#[derive(Elicit)]` |
//! | [`ElicitSpec`] | Agent-browsable contract spec | `impl_select_spec!` / `impl_builder_spec!` in `type_spec/` |
//! | `serde::Serialize` | Wire-format serialisation | `#[derive(Serialize)]` |
//! | `serde::Deserialize` | Wire-format deserialisation | `#[derive(Deserialize)]` |
//! | `schemars::JsonSchema` | JSON Schema generation for tooling | `#[derive(JsonSchema)]` |
//!
//! # Proof Composition Guarantee
//!
//! The most important obligation is carried by [`Elicitation`]. Its three proof
//! methods — `kani_proof()`, `verus_proof()`, `creusot_proof()` — have **no
//! default implementation**. Every type must supply them. For types derived with
//! `#[derive(Elicit)]` the macro generates them mechanically by iterating the
//! struct's fields:
//!
//! ```text
//! struct A { bar: Bar, baz: Baz }
//!
//! // Generated by the macro:
//! fn kani_proof() -> TokenStream {
//!     let mut ts = TokenStream::new();
//!     ts.extend(<Bar as Elicitation>::kani_proof()); // ← cannot be forgotten
//!     ts.extend(<Baz as Elicitation>::kani_proof()); // ← cannot be forgotten
//!     ts
//! }
//! ```
//!
//! This is the **provenance guarantee**: the macro sees the actual field types at
//! compile time, so delegation is structurally impossible to omit. Manual `impl`
//! blocks (primitives, third-party types) are on the honour system — the runtime
//! validation methods below exist to catch regressions there.
//!
//! # Composition Propagates Through Generics
//!
//! The bound `T: ElicitComplete` on generic containers means an incomplete inner
//! type blocks the whole chain:
//!
//! ```text
//! impl<T: ElicitComplete> ElicitComplete for Vec<T> {}
//! //        ↑ If T is incomplete, Vec<T> is also incomplete.
//! ```
//!
//! This is intentional: you cannot accidentally use a half-implemented type as an
//! element inside a verified container.
//!
//! # Runtime Validation (for Tests)
//!
//! Two families of methods are provided for use in integration tests:
//!
//! ## Non-emptiness (`validate_proofs_non_empty`)
//!
//! ```rust,ignore
//! // In tests/proof_non_empty_test.rs:
//! assert!(MyType::validate_proofs_non_empty(),
//!     "MyType has an empty proof — check the manual impl");
//! ```
//!
//! This catches the case where a manual impl returns `TokenStream::new()`, which
//! the type system cannot prevent because emptiness is a value property, not a
//! type property.
//!
//! ## Constituent delegation (`kani_proof_contains`)
//!
//! ```rust,ignore
//! // In tests/proof_composition_test.rs:
//! assert!(Container::<Inner>::kani_proof_contains::<Inner>(),
//!     "Container proof must include Inner's proof");
//! ```
//!
//! This catches regressions where a refactor removes a delegation call from a
//! manually-written proof body. It works by checking that
//! `Outer::kani_proof().to_string()` contains `Inner::kani_proof().to_string()`
//! as a substring.
//!
//! # Adding a New Type
//!
//! 1. Complete Phases 1–6 (see `THIRD_PARTY_SUPPORT_GUIDE.md`).
//! 2. Write `impl ElicitComplete for MyType {}`. Fix every compile error.
//! 3. Add `assert_proofs_non_empty::<MyType>("MyType")` to
//!    `crates/elicitation/tests/proof_non_empty_test.rs`.
//! 4. If `MyType` is an aggregate with a manual proof, add
//!    `assert_kani_contains::<MyType, FieldType>` to
//!    `crates/elicitation/tests/proof_composition_test.rs`.
//! 5. Run `just test-package elicitation` — all tests must pass.
//!
//! # Usage in Generic Bounds
//!
//! Use `ElicitComplete` as the single bound anywhere you need a fully-verified,
//! fully-introspectable, fully-serialisable elicitation type:
//!
//! ```rust,ignore
//! use elicitation::ElicitComplete;
//!
//! /// Register a type as an MCP tool parameter.
//! /// Only accepts types that have completed all framework obligations.
//! fn register_tool<T: ElicitComplete>(name: &str) { /* ... */ }
//!
//! /// A verified pipeline stage — T must be provably correct end-to-end.
//! struct Pipeline<T: ElicitComplete> { /* ... */ }
//! ```

use crate::{ElicitIntrospect, ElicitSpec, Elicitation};

/// Compiler-enforced supertrait for fully-implemented elicitation support.
///
/// `impl ElicitComplete for MyType {}` compiles only when every framework
/// obligation is satisfied. Use it as the single bound in generic code that
/// requires a type to be interactively elicitable, structurally introspectable,
/// formally verified, and wire-serialisable.
///
/// See the [module documentation][self] for the full design rationale, the
/// proof composition guarantee, and the step-by-step guide for adding new types.
pub trait ElicitComplete:
    Elicitation
    + ElicitIntrospect
    + ElicitSpec
    + serde::Serialize
    + for<'de> serde::Deserialize<'de>
    + schemars::JsonSchema
    + crate::emit_code::ToCodeLiteral
{
    /// Runtime check: all three proof methods return non-empty TokenStreams.
    ///
    /// Use in tests to catch any manual `impl Elicitation` that returns
    /// `TokenStream::new()`. Call this for every type in your test suite.
    ///
    /// # Example
    ///
    /// ```rust,ignore
    /// assert!(bool::validate_proofs_non_empty(), "bool proofs must be non-empty");
    /// ```
    fn validate_proofs_non_empty() -> bool {
        !Self::kani_proof().is_empty()
            && !Self::verus_proof().is_empty()
            && !Self::creusot_proof().is_empty()
    }

    /// Runtime check: does this type's Kani proof contain `Inner`'s Kani proof?
    ///
    /// Use this in tests to assert delegation — i.e., that an aggregate type's
    /// proof includes its constituent types' proofs. Catches regressions in
    /// manual proof implementations.
    ///
    /// # Example
    ///
    /// ```rust,ignore
    /// assert!(VecNonEmpty::<String>::kani_proof_contains::<String>(),
    ///     "VecNonEmpty proof must include String's proof");
    /// ```
    fn kani_proof_contains<Inner: Elicitation>() -> bool {
        let outer = Self::kani_proof().to_string();
        let inner = Inner::kani_proof().to_string();
        !inner.is_empty() && outer.contains(&inner)
    }

    /// Runtime check: does this type's Verus proof contain `Inner`'s Verus proof?
    fn verus_proof_contains<Inner: Elicitation>() -> bool {
        let outer = Self::verus_proof().to_string();
        let inner = Inner::verus_proof().to_string();
        !inner.is_empty() && outer.contains(&inner)
    }

    /// Runtime check: does this type's Creusot proof contain `Inner`'s Creusot proof?
    fn creusot_proof_contains<Inner: Elicitation>() -> bool {
        let outer = Self::creusot_proof().to_string();
        let inner = Inner::creusot_proof().to_string();
        !inner.is_empty() && outer.contains(&inner)
    }
}