Skip to content

THIRD_PARTY_SUPPORT_GUIDE.md

Latest commit

 

History

History
2343 lines (1812 loc) · 81.9 KB

THIRD_PARTY_SUPPORT_GUIDE.md

File metadata and controls

2343 lines (1812 loc) · 81.9 KB
Raw

Third-Party Crate Support Guide

This document is the authoritative checklist for adding elicitation support for a third-party crate. Follow every section in order. The clap integration is the canonical reference implementation for all patterns described here.

Core Verification Principle

Trust the source. Verify the wrapper.

This principle applies uniformly across all three verifiers (Kani, Creusot, Verus) and to all type origins (std lib, third-party crates, our own contract types):

  • Trust the source — assume the stdlib and third-party crates uphold their own invariants. We do not re-verify that clap::ColorChoice has exactly three variants, or that std::collections::HashMap correctly stores keys. That is the responsibility of the upstream library and its own test suite.

  • Verify the wrapper — prove that our business logic is correct: that every label produced by labels() is accepted by from_label(), that the roundtrip is complete, that unknown inputs are rejected, that our Elicitation impl delegates correctly.

This keeps proofs focused, tractable, and meaningful. A kani::assume(true) for a third-party builder type is not a cop-out — it is an explicit, documented architectural decision that we have placed that type in the "trusted" category and are not claiming to verify its internals.

Overview

Adding full support for a third-party crate foo involves work across six locations:

Location What you add
Cargo.toml (workspace root) Optional dep + elicit_foo workspace member
crates/elicitation/ Elicitation trait impls (feature-gated foo-types)
crates/elicit_foo/ Newtypes + reflect_methods + (optionally) trait factories
crates/elicitation_kani/ Kani proof harnesses
crates/elicitation_creusot/ Creusot #[requires]/#[ensures]/#[trusted] proofs
crates/elicitation_verus/ Verus ensures/requires proofs

There are five distinct mechanisms for exposing types as MCP tools:

Mechanism Use when Location
#[reflect_methods] Your newtype has methods you want to expose elicitation_derive
#[reflect_trait] A third-party trait has methods worth calling on any T: FooTrait elicitation_macros
Fragment tool + EmitCode A Rust macro (or closure/expression) that runs at compile time, not at runtime elicitation::emit_code
Descriptor-registry plugin A code-generation-target crate (tower, axum, winit) — types cannot be instantiated over MCP; all value is in code recovery Phase 3E
Factory pattern for generics A generic API Foo<T> where T: ElicitComplete — generates per-type tools at startup Phase 3F

The fragment tool mechanism bypasses Phases 2, 4, 5, and 6 — no Elicitation trait impls, no Kani/Creusot/Verus verification. See the Fragment Tools section.

The descriptor-registry and factory patterns (Phases 3E/3F) similarly bypass verification Phases 4–6 for descriptor types — kani::assume(true) is correct for types whose value is entirely in code recovery, not runtime execution.

Never skip a section. Never add an #[allow] attribute. Fix root causes.

Common mistake — skipping Phase 2 in favour of the shadow crate. It is tempting to jump straight to crates/elicit_foo/ (Phase 3) because that is where the visible MCP tools live. Resist this. Phase 2 is the foundation: without impl Elicitation for foo::MyType in crates/elicitation/, the shadow crate has no interactive elicitation behaviour to delegate to. The shadow crate adds JSON-schema support and transport; Phase 2 adds the reasoning — the prompts, the Select options, the proof stubs. Phase 2 must come before Phase 3, every time.

Phase 1 — Workspace Root (Cargo.toml)

# Add to [workspace.dependencies]
foo = { version = "X.Y", features = ["..."] }
elicit_foo = { path = "crates/elicit_foo", version = "0.9" }

# Add to [workspace.members]
"crates/elicit_foo",

Notes:

  • Match the version constraint convention: major-only for >=1.0, major.minor for >=0.1.0
  • Add all features the Elicitation impls will need (e.g. "string" for clap::Id)
  • Do not add elicit_foo to default-members unless it has its own binary

Phase 2 — Core Trait Impls in crates/elicitation/

2.1 Feature flag

In crates/elicitation/Cargo.toml:

[dependencies]
foo = { workspace = true, optional = true }

[features]
foo-types = ["dep:foo"]

2.2 Type files

Create crates/elicitation/src/primitives/foo_types/ with one file per type.

For Select enum types (user picks from a fixed list):

// src/primitives/foo_types/my_enum.rs
use crate::{
    ElicitCommunicator, ElicitError, ElicitErrorKind, ElicitIntrospect, ElicitResult,
    Elicitation, ElicitationPattern, PatternDetails, Prompt, Select, TypeMetadata,
    VariantMetadata, mcp,
};
use foo::MyEnum;

impl Prompt for MyEnum {
    fn prompt() -> Option<&'static str> {
        Some("Choose a MyEnum value:")
    }
}

impl Select for MyEnum {
    fn options() -> Vec<Self> {
        vec![MyEnum::VariantA, MyEnum::VariantB]
    }

    fn labels() -> Vec<String> {
        vec!["Variant A description".to_string(), "Variant B description".to_string()]
    }

    fn from_label(label: &str) -> Option<Self> {
        match label {
            "Variant A description" => Some(MyEnum::VariantA),
            "Variant B description" => Some(MyEnum::VariantB),
            _ => None,
        }
    }
}

crate::default_style!(MyEnum => MyEnumStyle);

impl Elicitation for MyEnum {
    type Style = MyEnumStyle;

    #[tracing::instrument(skip(communicator))]
    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
        let params = mcp::select_params(
            Self::prompt().unwrap_or("Choose value:"),
            &Self::labels(),
        );
        let result = communicator
            .call_tool(
                rmcp::model::CallToolRequestParams::new(mcp::tool_names::elicit_select())
                    .with_arguments(params),
            )
            .await?;
        let value = mcp::extract_value(result)?;
        let label = mcp::parse_string(value)?;
        Self::from_label(&label).ok_or_else(|| {
            ElicitError::new(ElicitErrorKind::ParseError(format!(
                "Invalid MyEnum: {}", label
            )))
        })
    }
}

impl ElicitIntrospect for MyEnum {
    fn pattern() -> ElicitationPattern { ElicitationPattern::Select }

    fn metadata() -> TypeMetadata {
        TypeMetadata {
            type_name: "foo::MyEnum",
            description: Self::prompt(),
            details: PatternDetails::Select {
                variants: Self::labels()
                    .into_iter()
                    .map(|label| VariantMetadata { label, fields: vec![] })
                    .collect(),
            },
        }
    }
}

For text/primitive types (user types a value):

impl Elicitation for MyType {
    type Style = MyTypeStyle;

    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
        let params = mcp::text_params(Self::prompt().unwrap_or("Enter value:"));
        let result = communicator
            .call_tool(
                rmcp::model::CallToolRequestParams::new(mcp::tool_names::elicit_text())
                    .with_arguments(params),
            )
            .await?;
        let value = mcp::extract_value(result)?;
        let s = mcp::parse_string(value)?.trim().to_string();
        MyType::new(s).map_err(|e| ElicitError::new(ElicitErrorKind::ParseError(e.to_string())))
    }
}

Key rules for both patterns:

  • .trim().to_string() before passing to constructors — .trim() returns &str, but constructors need String (no From<&str> without 'static)
  • Use mcp::select_params + elicit_select for enums
  • Use mcp::text_params + elicit_text for primitives/survey types
  • #[tracing::instrument(skip(communicator))] on all async fn elicit
  • Never use #[allow] — gate feature-dependent code with #[cfg(feature = "foo-types")]

2.3 Module wiring

In src/primitives/mod.rs:

#[cfg(feature = "foo-types")]
pub mod foo_types;

In src/lib.rs:

#[cfg(feature = "foo-types")]
pub use primitives::foo_types::{MyEnum, MyType, /* ... */};

2.4 TypeSpec (ElicitSpec) in src/type_spec/

Create src/type_spec/foo_specs.rs. This adds agent-browsable contract descriptions to the global inventory, complementing the structural metadata from ElicitIntrospect. Agents use this via the describe_type / explore_type MCP tools.

Two macros handle the boilerplate:

//! ElicitSpec impls for foo types. Available with the `foo-types` feature.

#[cfg(feature = "foo-types")]
mod foo_impls {
    use crate::{
        ElicitSpec, SpecCategoryBuilder, SpecEntryBuilder, TypeSpec, TypeSpecBuilder,
        TypeSpecInventoryKey,
    };

    // For Select enums — list each variant with a description
    macro_rules! impl_select_spec {
        (
            type    = $ty:ty,
            name    = $name:literal,
            summary = $summary:literal,
            variants = [$(($label:literal, $desc:literal)),+ $(,)?]
        ) => {
            impl ElicitSpec for $ty {
                fn type_spec() -> TypeSpec {
                    let variants = SpecCategoryBuilder::default()
                        .name("variants".to_string())
                        .entries(vec![
                            $(
                                SpecEntryBuilder::default()
                                    .label($label.to_string())
                                    .description($desc.to_string())
                                    .build()
                                    .expect("valid SpecEntry"),
                            )+
                        ])
                        .build()
                        .expect("valid SpecCategory");
                    let source = SpecCategoryBuilder::default()
                        .name("source".to_string())
                        .entries(vec![
                            SpecEntryBuilder::default()
                                .label("crate".to_string())
                                .description("foo — third-party crate".to_string())
                                .build()
                                .expect("valid SpecEntry"),
                            SpecEntryBuilder::default()
                                .label("pattern".to_string())
                                .description("Select — choose one variant from the list".to_string())
                                .build()
                                .expect("valid SpecEntry"),
                        ])
                        .build()
                        .expect("valid SpecCategory");
                    TypeSpecBuilder::default()
                        .type_name($name.to_string())
                        .summary($summary.to_string())
                        .categories(vec![variants, source])
                        .build()
                        .expect("valid TypeSpec")
                }
            }
            inventory::submit!(TypeSpecInventoryKey::new(
                $name,
                <$ty as ElicitSpec>::type_spec,
                std::any::TypeId::of::<$ty>
            ));
        };
    }

    // For builder/struct types — list key fields
    macro_rules! impl_builder_spec {
        (
            type    = $ty:ty,
            name    = $name:literal,
            summary = $summary:literal,
            fields  = [$(($label:literal, $desc:literal)),+ $(,)?]
        ) => {
            impl ElicitSpec for $ty {
                fn type_spec() -> TypeSpec {
                    let fields = SpecCategoryBuilder::default()
                        .name("fields".to_string())
                        .entries(vec![
                            $(
                                SpecEntryBuilder::default()
                                    .label($label.to_string())
                                    .description($desc.to_string())
                                    .build()
                                    .expect("valid SpecEntry"),
                            )+
                        ])
                        .build()
                        .expect("valid SpecCategory");
                    let source = SpecCategoryBuilder::default()
                        .name("source".to_string())
                        .entries(vec![
                            SpecEntryBuilder::default()
                                .label("crate".to_string())
                                .description("foo — third-party crate".to_string())
                                .build()
                                .expect("valid SpecEntry"),
                            SpecEntryBuilder::default()
                                .label("pattern".to_string())
                                .description("Survey — builder type elicited field by field".to_string())
                                .build()
                                .expect("valid SpecEntry"),
                        ])
                        .build()
                        .expect("valid SpecCategory");
                    TypeSpecBuilder::default()
                        .type_name($name.to_string())
                        .summary($summary.to_string())
                        .categories(vec![fields, source])
                        .build()
                        .expect("valid TypeSpec")
                }
            }
            inventory::submit!(TypeSpecInventoryKey::new(
                $name,
                <$ty as ElicitSpec>::type_spec,
                std::any::TypeId::of::<$ty>
            ));
        };
    }

    impl_select_spec!(
        type    = foo::MyEnum,
        name    = "foo::MyEnum",
        summary = "One-line description of what MyEnum controls.",
        variants = [
            ("VariantA", "Description of what VariantA does"),
            ("VariantB", "Description of what VariantB does"),
        ]
    );

    impl_builder_spec!(
        type    = foo::MyBuilder,
        name    = "foo::MyBuilder",
        summary = "One-line description of the builder type.",
        fields = [
            ("field_one", "What field_one controls"),
            ("field_two", "What field_two controls"),
        ]
    );
}

Then wire the new file in src/type_spec/mod.rs:

mod foo_specs;

The module declaration is unconditional — the #[cfg(feature = "foo-types")] lives inside the file. This matches the pattern of all other *_specs.rs files.

Phase 3 — Wrapper Crate crates/elicit_foo/

3.1 Cargo.toml

[package]
name = "elicit_foo"
version.workspace = true
edition.workspace = true
# ... other workspace fields

[dependencies]
elicitation = { workspace = true, features = ["foo-types"] }
elicitation_derive = { workspace = true }
foo = { workspace = true }
schemars = { workspace = true }
tracing = { workspace = true }
rmcp = { workspace = true }

3.2 src/lib.rs

//! Elicitation-enabled newtype wrappers for the `foo` crate.
//!
//! Each wrapper provides:
//! - Implements [`schemars::JsonSchema`] so the type can appear in MCP tool schemas
//! - Transparent [`Deref`]/[`DerefMut`] access to the inner type
//! - [`reflect_methods`] impl exposing public API as MCP tools

mod my_enum;
mod my_type;

pub use my_enum::MyEnum;
pub use my_type::MyType;

3.3 Type files

Template for all types:

//! [`foo::MyType`] newtype wrapper.

use elicitation::{elicit_newtype, elicit_newtype_traits};
use elicitation_derive::reflect_methods;

elicit_newtype!(foo::MyType, as MyType);
// Add trait flags as applicable. Common flags:
// [eq]       → PartialEq + Eq
// [eq_hash]  → PartialEq + Eq + Hash
// [ord]      → PartialEq + Eq + PartialOrd + Ord
// [cmp]      → PartialEq + Eq + Hash + PartialOrd + Ord
// [display]  → Display
// [from_str] → FromStr
elicit_newtype_traits!(MyType, foo::MyType, [eq, display]);

#[reflect_methods]
impl MyType {
    /// Short description.
    #[tracing::instrument(skip(self))]
    pub fn some_method(&self) -> ReturnType {
        self.0.some_method()
    }
}

Key rules:

  • elicit_newtype! generates: Arc<T> wrapper struct + generic object JsonSchema + Deref/DerefMut/AsRef/From impls — do not add a custom JsonSchema impl; the macro's object schema is correct for MCP
  • elicit_newtype_traits! only lists traits the inner type actually implements — check the crate docs
  • All methods in #[reflect_methods] must be pub, #[tracing::instrument(skip(self))], return owned types (not references into inner type — return String not &str, Option<String> not Option<&str>)
  • Do not wrap methods that return crate-internal types with no JsonSchema — return String equivalents instead
  • For #[non_exhaustive] enums, add a _ => "Unknown" wildcard arm in match expressions

elicit_newtype! variants:

Syntax JsonSchema Serialize/Deserialize
elicit_newtype!(T, as Name) Generic object schema (use this) No
elicit_newtype!(T, as Name, serde) Delegated to T Yes (T: Serialize)

Never add no_schema — that variant was removed because the object schema is what MCP needs.

Phase 3B — Trait Factories (#[reflect_trait])

Use this phase when the third-party crate exposes derive traits (like clap::ValueEnum, clap::CommandFactory) whose methods are worth calling as standalone MCP tools — independently of any particular instance of the newtype wrapper.

Skip this phase if no derive traits are worth exposing.

3B.1 When to use #[reflect_trait] vs #[reflect_methods]

Situation Use
You own a newtype and want to expose its methods #[reflect_methods] on impl MyType
A third-party trait has static or instance methods you want callable for any T: FooTrait #[reflect_trait(foo::FooTrait)]
Both Both — they compose

#[reflect_trait] generates a factory: a struct that implements AnyToolFactory and is submitted to inventory at link time. At runtime, the DynamicToolRegistry discovers all factories, and the agent can instantiate tools for any registered concrete type.

3B.2 The orphan rule and type_map

The orphan rule prevents writing impl ElicitProxy for foo::ForeignType in elicit_foo (neither trait nor type is local). The type_map attribute solves this by substituting foreign types with your elicit_foo newtype wrappers that already have the right From impls:

// WRONG — orphan rule violation, won't compile:
impl ElicitProxy for foo::Command { ... }

// CORRECT — use type_map to declare the substitution:
#[reflect_trait(foo::CommandFactory,
    type_map(foo::Command => crate::Command))]
pub trait CommandFactoryTools {
    fn command() -> foo::Command;
}
// The macro uses crate::Command in the param struct and generates
// foo::Command::from(crate_command) / crate::Command::from(foo_command) conversions.

Requirements for a mapped type:

  • The proxy type must implement Serialize + Deserialize + JsonSchema
  • From<ProxyType> for OriginalType must exist (for params going in)
  • From<OriginalType> for ProxyType must exist (for return values coming out)

elicit_newtype! already provides From<Original> for Wrapper (wraps in Arc) and From<Wrapper> for Arc<Original>. You must manually add From<Wrapper> for Original for the param direction — see the command.rs, id.rs, possible_value.rs files in elicit_clap for the pattern (use Arc::try_unwrap with clone fallback).

3B.3 ElicitProxy for stdlib and user-owned types

For types that don't need type_map — stdlib types and types you own — implement ElicitProxy instead:

// For types you own — use the derive macro:
use elicitation_derive::ElicitProxy;

#[derive(Debug, Clone, Serialize, Deserialize, JsonSchema, Elicit, ElicitProxy)]
pub struct MyConfig { pub name: String }

ElicitProxy is already implemented for all stdlib primitives, String, Vec<T>, Option<T>, Result<T, E>, and common types. You only need to implement it for your own domain types.

Do not implement ElicitProxy for foreign types — use type_map instead.

3B.4 Macro syntax

use elicitation_macros::reflect_trait;

// Simplest form — no type substitution needed:
#[reflect_trait(foo::MyTrait)]
pub trait MyTraitTools {
    fn static_method(arg: String) -> bool;
    fn instance_method(&self, arg: i32) -> String;
}

// With type substitution (orphan-rule workaround):
#[reflect_trait(foo::MyTrait,
    type_map(foo::TypeA => crate::TypeA, foo::TypeB => crate::TypeB))]
pub trait MyTraitTools {
    fn method_a(input: foo::TypeA) -> foo::TypeB;
}

Syntax notes:

  • The marker trait block is consumed by the macro — it is not emitted as a real trait
  • Method signatures must match the real trait exactly (same names, same types)
  • &self receivers are supported — the agent passes {"target": <serialized T>} in the params
  • &str params are automatically handled: the param struct stores String, the vtable calls .as_str()
  • &[T] return types are automatically handled: .to_vec() is called to make them owned
  • Multiple type_map entries are comma-separated

What the macro generates:

  • One param struct per method (implements Deserialize + JsonSchema)
  • A vtable struct with one Arc<dyn Fn(Value) -> BoxFuture<...>> per method
  • A factory struct implementing AnyToolFactory
  • An inventory::submit! call registering the factory at link time
  • A free pub fn prime_foo__mytrait::<T>() function for startup registration

3B.5 Naming conventions

The generated names are derived from the fully-qualified trait path:

Input Generated name
foo::MyTrait Factory: MyTraitFactory, prime fn: prime_foo__my_trait::<T>()
clap::ValueEnum Factory: ValueEnumFactory, prime fn: prime_clap__value_enum::<T>()
clap::CommandFactory Factory: CommandFactoryFactory, prime fn: prime_clap__command_factory::<T>()

Tool names at runtime: {prefix}__{method_name} — e.g. myapp__value_variants.

3B.6 Startup registration (prime + register_type)

At server startup, for each concrete type T implementing the trait:

use elicit_foo::trait_factories::prime_foo__my_trait;
use elicitation::DynamicToolRegistry;

// Prime each factory for each type (monomorphizes the vtable closures)
prime_foo__my_trait::<MyConcreteType>();

// Register each type under a prefix
let registry = DynamicToolRegistry::new()
    .register_type::<MyConcreteType>("mytype");

// The agent calls the factory meta-tool to instantiate tools at runtime:
// registry.instantiate("foo::MyTrait", "mytype").await?;
// → creates "mytype__method_one", "mytype__method_two", etc.

The agent sees factory meta-tools in list_tools immediately. After calling a meta-tool (or registry.instantiate(...) programmatically), the method tools appear in list_tools.

3B.7 Cargo.toml additions for trait factories

[dependencies]
elicitation_macros = { workspace = true }
inventory = { workspace = true }
serde_json = { workspace = true }

[dev-dependencies]
tokio = { workspace = true }
serde_json = { workspace = true }

3B.8 Testing trait factories

Each trait factory must be tested at three levels (see crates/elicit_clap/tests/trait_factories_test.rs):

use elicit_foo::trait_factories::prime_foo__my_trait;
use elicitation::{DynamicToolRegistry, Elicit, ElicitPlugin, ToolFactoryRegistration};

// 1. Inventory registration
#[test]
fn my_trait_factory_in_inventory() {
    let found = inventory::iter::<ToolFactoryRegistration>
        .into_iter()
        .any(|r| r.trait_name == "foo::MyTrait");
    assert!(found);
}

// 2. Prime + instantiate lifecycle
#[tokio::test]
async fn my_trait_instantiate_creates_tools() {
    prime_foo__my_trait::<MyConcreteType>();
    let registry = DynamicToolRegistry::new()
        .register_type::<MyConcreteType>("t");
    registry.instantiate("foo::MyTrait", "t").await.unwrap();
    let names: Vec<_> = registry.list_tools().iter()
        .map(|t| t.name.to_string()).collect();
    assert!(names.contains(&"t__method_name".to_string()));
}

// 3. Handler invocation
#[tokio::test]
async fn my_trait_method_returns_expected_value() {
    prime_foo__my_trait::<MyConcreteType>();
    let registry = DynamicToolRegistry::new()
        .register_type::<MyConcreteType>("t");
    registry.instantiate("foo::MyTrait", "t").await.unwrap();
    let result = registry
        .invoke_dynamic("t__method_name", serde_json::json!({"arg": "value"}))
        .await.expect("tool exists").expect("tool succeeds");
    // check result content...
}

Use DynamicToolRegistry::invoke_dynamic(name, args) to call tools directly without an MCP connection.

3B.9 Deferred traits

Some traits cannot be exposed as MCP tools because their method signatures are fundamentally incompatible:

Trait Blocker
clap::FromArgMatches Takes &ArgMatches — not Serialize, not Clone
clap::Parser Extends FromArgMatches — same blocker
Any trait with &mut self methods that borrow internal state Mutable borrows conflict with Arc<T> wrapper

For these, document the deferral in a comment at the top of trait_factories.rs.

3B.10 clap reference implementation

// crates/elicit_clap/src/trait_factories.rs

use elicitation_macros::reflect_trait;

#[reflect_trait(clap::CommandFactory,
    type_map(clap::Command => crate::Command))]
pub trait CommandFactoryTools {
    fn command() -> clap::Command;
    fn command_for_update() -> clap::Command;
}

#[reflect_trait(clap::Subcommand,
    type_map(clap::Command => crate::Command))]
pub trait SubcommandTools {
    fn augment_subcommands(cmd: clap::Command) -> clap::Command;
    fn augment_subcommands_for_update(cmd: clap::Command) -> clap::Command;
    fn has_subcommand(name: &str) -> bool;
}

#[reflect_trait(clap::ValueEnum,
    type_map(clap::builder::PossibleValue => crate::PossibleValue))]
pub trait ValueEnumTools {
    fn value_variants() -> &'static [Self];
    fn to_possible_value(&self) -> Option<clap::builder::PossibleValue>;
    fn from_str(input: &str, ignore_case: bool) -> Result<Self, String>;
}

#[reflect_trait(clap::Args,
    type_map(clap::Command => crate::Command, clap::Id => crate::Id))]
pub trait ArgsTools {
    fn augment_args(cmd: clap::Command) -> clap::Command;
    fn augment_args_for_update(cmd: clap::Command) -> clap::Command;
    fn group_id() -> Option<clap::Id>;
}

User-side startup:

use elicit_clap::trait_factories::{
    prime_clap__command_factory,
    prime_clap__value_enum,
    prime_clap__args,
    prime_clap__subcommand,
};

// Call once per type at startup:
prime_clap__command_factory::<MyCli>();
prime_clap__value_enum::<MyOutputFormat>();
prime_clap__args::<MyArgs>();
prime_clap__subcommand::<MySubcmd>();

let registry = DynamicToolRegistry::new()
    .register_type::<MyCli>("cli")
    .register_type::<MyOutputFormat>("fmt")
    .register_type::<MyArgs>("args")
    .register_type::<MySubcmd>("cmd");

Phase 3C — Verified Workflow Plugin

Use this phase when the third-party library is stateful — it requires connection pools, sessions, open transactions, or any other server-side state that persists across MCP tool calls. Skip this phase for stateless libraries.

The canonical example is elicit_sqlx/src/workflow.rs (SqlxWorkflowPlugin).

3C.1 Propositions

Each observable invariant that a tool can establish is a unit struct implementing Prop:

use elicitation::contracts::{And, Established, Prop, both};

pub struct DbConnected;
impl Prop for DbConnected {}

pub struct QueryExecuted;
impl Prop for QueryExecuted {}

pub struct TransactionOpen;
impl Prop for TransactionOpen {}

// Composite propositions for multi-step proofs:
pub type ConnectedAndExecuted = And<DbConnected, QueryExecuted>;

Tools signal that they have established a proposition by binding an Established<P> return value inside the function:

let _proof: Established<QueryExecuted> = Established::assert();

Established<P> is a zero-cost PhantomData marker — it disappears at compile time and carries no runtime cost.

3C.2 Context types

Define three layers:

Context type Scope Holds
FooCtx (plugin) Entire plugin lifetime Shared state maps — pools, sessions, etc.
FooPoolCtx (per-call) Resolved at call time Single pre-resolved resource
FooTxCtx (per-call) Created by begin, consumed by commit/rollback Open transaction 
use dashmap::DashMap;
use tokio::sync::Mutex;

pub struct FooCtx {
    pools: Mutex<HashMap<Uuid, Pool>>,
    txs:   Mutex<HashMap<Uuid, Arc<FooTxCtx>>>,
}

pub struct FooPoolCtx { pub pool: Pool }
pub struct FooTxCtx   { tx: Mutex<Option<Transaction>> }

3C.3 Tool functions

Write each tool as an individual #[elicit_tool]-annotated async function. Do not write a monolithic dispatcher — that prevents the macro from generating descriptors and EmitCode.

use elicitation::elicit_tool;

#[elicit_tool(
    plugin = "foo_workflow",
    name   = "foo_workflow__connect",
    description = "Open a connection pool.  Establishes: FooConnected."
)]
async fn wf_connect(ctx: Arc<FooCtx>, p: WfConnectParams) -> Result<CallToolResult, ErrorData> {
    let pool = Pool::connect(&p.url).await
        .map_err(|e| ErrorData::internal_error(e.to_string(), None))?;
    let pool_id = Uuid::new_v4();
    ctx.pools.lock().await.insert(pool_id, pool);
    Ok(json_result(&WfConnectResult { pool_id }))
}

3C.4 Manual impl ElicitPlugin

Use #[derive(ElicitPlugin)] only when every tool in the plugin takes the same context type. For workflow plugins, different tools need different context objects — use a manual impl instead.

pub struct FooWorkflowPlugin(Arc<FooCtx>);

impl elicitation::ElicitPlugin for FooWorkflowPlugin {
    fn name(&self) -> &'static str { "foo_workflow" }

    fn list_tools(&self) -> Vec<Tool> {
        // inventory collects all #[elicit_tool(plugin = "foo_workflow", ...)] registrations
        elicitation::inventory::iter::<elicitation::PluginToolRegistration>()
            .filter(|r| r.plugin == "foo_workflow")
            .map(|r| (r.constructor)().as_tool())
            .collect()
    }

    fn call_tool<'a>(
        &'a self,
        params: CallToolRequestParams,
        _ctx: RequestContext<rmcp::RoleServer>,
    ) -> BoxFuture<'a, Result<CallToolResult, ErrorData>> {
        let plugin_ctx = self.0.clone();
        Box::pin(async move {
            let name  = params.name.as_ref();
            let bare  = name.strip_prefix("foo_workflow__").unwrap_or(name);
            let full  = format!("foo_workflow__{bare}");

            // Resolve descriptor from inventory (full name lookup).
            let descriptor = elicitation::inventory::iter::<elicitation::PluginToolRegistration>()
                .filter(|r| r.plugin == "foo_workflow")
                .find(|r| r.name == full)
                .map(|r| (r.constructor)())
                .ok_or_else(|| ErrorData::invalid_params(format!("unknown tool: {name}"), None))?;

            // Resolve per-call context based on tool group.
            let tool_ctx: Arc<dyn std::any::Any + Send + Sync> = match bare {
                "connect" | "disconnect" => {
                    plugin_ctx.clone() as Arc<dyn std::any::Any + Send + Sync>
                }
                "execute" | "fetch_all" => {
                    let p: WfPoolIdParams = parse_args(&params)?;
                    let pool = plugin_ctx.pools.lock().await
                        .get(&p.pool_id).cloned()
                        .ok_or_else(|| ErrorData::invalid_params("pool_id not found", None))?;
                    Arc::new(FooPoolCtx { pool }) as Arc<dyn std::any::Any + Send + Sync>
                }
                "commit" | "rollback" => {
                    let p: WfTxIdParams = parse_args(&params)?;
                    plugin_ctx.txs.lock().await
                        .remove(&p.tx_id)
                        .ok_or_else(|| ErrorData::invalid_params("tx_id not found", None))?
                        as Arc<dyn std::any::Any + Send + Sync>
                }
                _ => return Err(ErrorData::invalid_params(format!("unknown tool: {bare}"), None)),
            };

            descriptor.dispatch(tool_ctx, params).await
        })
    }
}

Key rules:

  • list_tools() queries inventory — zero maintenance as tools are added
  • call_tool() only resolves which context type to pass — no tool logic lives here
  • Session-state tools (connect, begin): pass Arc<FooCtx> directly
  • Resource-using tools (execute, tx_*): look up and pass a narrowed Arc<FooPoolCtx> or Arc<FooTxCtx>
  • Consuming tools (commit, rollback): remove from map so the resource is dropped

3C.5 Public API methods

Add pub async fn methods to the plugin struct for use in tests and in Rust code that uses the plugin directly (not via MCP):

impl FooWorkflowPlugin {
    pub async fn connect(&self, url: &str) -> Result<(Uuid, Established<FooConnected>), String> {
        let pool = Pool::connect(url).await.map_err(|e| e.to_string())?;
        let id = Uuid::new_v4();
        self.0.pools.lock().await.insert(id, pool);
        Ok((id, Established::assert()))
    }
}

3C.6 Cargo.toml additions

[dependencies]
elicitation_derive = { workspace = true }
futures            = { workspace = true }
proc-macro2        = { workspace = true }
quote              = { workspace = true }
inventory          = { workspace = true }
tokio              = { workspace = true, features = ["sync"] }
uuid               = { workspace = true }

Phase 3D — EmitCode for Workflow Tools

The #[elicit_tool] macro auto-generates EmitCode — do not write impl EmitCode manually for tool functions.

3D.1 Two emit modes

Attribute When to use
emit = auto (default) Handler body translates cleanly to standalone binary code
emit = MyCustomType Tool creates/stores session state, or uses patterns the auto-rewriter can't handle

Auto-emit transforms the handler body:

  • p.field → binds the param value inline
  • ctx.method() → replaced by the emit_ctx expression
  • ErrorData::method(msg, ...) → std::io::Error::new(std::io::ErrorKind::Other, msg)
  • Ok(CallToolResult::success(...)) → println!(...)

Custom emit is required for tools whose MCP handler logic is fundamentally different from the code that makes sense in a standalone binary. Examples:

  • connect: MCP handler stores the pool in a session map by UUID; the binary just holds a local variable pool
  • begin: MCP handler stores a transaction by UUID; the binary just does let mut tx = pool.begin().await?
  • tx_fetch_*: uses &mut **tx deref patterns that the auto-rewriter can't construct

3D.2 CustomEmit<P> pattern

For tools that need custom emit, write a zero-sized marker type co-located with the tool function:

pub struct WfConnectEmit;
impl CustomEmit<WfConnectParams> for WfConnectEmit {
    fn emit_code(p: &WfConnectParams) -> TokenStream {
        let url      = p.database_url.as_str();
        let max_conn = p.max_connections.unwrap_or(10);
        quote! {
            let pool = AnyPoolOptions::new()
                .max_connections(#max_conn)
                .connect(#url)
                .await?;
        }
    }
}

#[elicit_tool(
    plugin = "foo_workflow",
    name   = "foo_workflow__connect",
    description = "...",
    emit = WfConnectEmit   // ← tell the macro which CustomEmit to use
)]
async fn wf_connect(ctx: Arc<FooCtx>, p: WfConnectParams) -> Result<CallToolResult, ErrorData> {
    // ... runtime handler body (NOT code generation) ...
}

#[elicit_tool] sees emit = WfConnectEmit and generates the EmitCode delegation automatically. You never write impl EmitCode yourself.

3D.3 EmitEntry inventory (for emit_dispatch_crate)

The PluginToolRegistration inventory (managed by #[elicit_tool]) handles interactive tool calls. The EmitEntry inventory is a separate registry used by emit_dispatch_crate in elicit_server to reconstruct a standalone binary from a recorded tool call log (the N→1 pipeline).

Register each workflow tool manually:

use elicitation::emit_code::{CrateDep, EmitCode, EmitEntry};

const FOO_DEP: CrateDep = CrateDep {
    name: "foo",
    version: "1",
    features: &[],
};

// Thin newtype so EmitCode can be object-safe.
struct WfConnectEmitEntry(WfConnectParams);
impl EmitCode for WfConnectEmitEntry {
    fn emit_code(&self) -> TokenStream { WfConnectEmit::emit_code(&self.0) }
    fn crate_deps(&self) -> Vec<CrateDep> { vec![FOO_DEP] }
}

inventory::submit! {
    EmitEntry {
        tool:       "foo_workflow__connect",
        crate_name: "elicit_foo",
        constructor: |v| {
            serde_json::from_value::<WfConnectParams>(v)
                .map(|p| Box::new(WfConnectEmitEntry(p)) as Box<dyn EmitCode>)
                .map_err(|e| e.to_string())
        },
    }
}

One inventory::submit! block per tool. Tools with no params use |_v| Ok(Box::new(...)).

3D.4 Linkage anchor in elicit_server

emit_dispatch_crate in elicit_server must link the elicit_foo CGUs or the inventory submissions will be dead-stripped. Add a size_of anchor:

// In elicit_server/src/lib.rs, inside emit_dispatch_crate():
let _ = std::mem::size_of::<elicit_foo::workflow::WfConnectParams>();

And add the dependency:

# elicit_server/Cargo.toml
[dependencies]
elicit_foo = { workspace = true }

3D.5 Reference implementation

crates/elicit_sqlx/src/workflow.rs — 13 workflow tools:

  • 2 tools with emit = auto (disconnect, commit/rollback — trivial bodies)
  • 11 tools with emit = WfXxxEmit (custom — session state or deref patterns)
  • 13 inventory::submit!(EmitEntry {...}) blocks

Phase 3E — Descriptor-Registry Plugin (Code-Generation-Target Crates)

Use this phase when the third-party library is a code-generation target — its types cannot be instantiated or called over an MCP boundary at runtime. The entire value is in code recovery: the agent assembles serializable descriptor structs, stores them by UUID, then uses ToCodeLiteral/EmitCode to recover the Rust source that creates them.

Examples: tower, axum, winit, wgpu, leptos.

Contrast with Phase 3C (workflow plugin): workflow plugins hold live resources (pools, connections, transactions). Descriptor-registry plugins hold config descriptors — pure data that maps back to Rust source.

3E.1 Decide: descriptor crate vs. inline plugin

For libraries whose types are entirely serializable configs (no live resources), the entire plugin can live in crates/elicit_foo/ without a workflow module. Use a single lib.rs with one or more plugin modules.

For libraries with a mix of config types and live resources, split:

  • Descriptor plugins in crates/elicit_foo/src/ (one file per domain)
  • Workflow plugin in crates/elicit_foo/src/workflow.rs (Phase 3C pattern)

3E.2 Descriptor types in crates/elicitation/src/primitives/foo_types/

Each descriptor type is a serializable mirror of a third-party config. Design rules:

1. One field per config knob, primitive Rust types only.

/// Descriptor for `tower::timeout::TimeoutLayer`.
#[derive(Debug, Clone, PartialEq,
    serde::Serialize, serde::Deserialize, schemars::JsonSchema,
    elicitation_derive::ToCodeLiteral)]
pub struct TowerTimeoutLayer {
    /// Timeout in milliseconds.
    pub timeout_millis: u64,
}

2. Closure/fn/macro fields use String — same as body: String in fragment tools.

Store the full Rust expression as a string. The field can hold a closure ("|e| e.to_string()"), a function name ("my_fn"), or a macro invocation ("vec![1, 2, 3]"). On emit, parse with .parse::<TokenStream>() and splice into quote!. Do NOT write From impls for closure-typed fields — closures cannot be instantiated at runtime.

/// Descriptor for `tower::util::MapErrLayer<F>`.
#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize,
    schemars::JsonSchema, elicitation_derive::ToCodeLiteral)]
pub struct TowerMapErrLayer {
    /// Rust expression for the error-mapping fn (closure or named fn).
    /// Examples: `"|e| e.to_string()"`, `"my_mapper"`.
    pub mapper_fn: String,
}

Field prompts must say "Rust expression (closure or fn name, e.g. |e| e.to_string())" — not just "Rust identifier". Closures, function names, and macro calls are all valid.

3. Generic type parameters become String fields storing the type expression.

/// Factory config for `tower::util::BoxService<Req, Resp, Err>`.
pub struct TowerBoxServiceConfig {
    pub req_type: String,   // e.g. "http::Request<hyper::Body>"
    pub resp_type: String,  // e.g. "http::Response<hyper::Body>"
    pub err_type: String,   // e.g. "Box<dyn std::error::Error>"
}

4. Implement ElicitComplete — use the compiler as your checklist.

impl ElicitComplete for TowerTimeoutLayer {}

The compiler rejects this if any supertrait (Elicitation, ElicitIntrospect, ElicitSpec, Serialize, Deserialize, JsonSchema) is missing. Do not paper over errors with #[allow] — follow each error to its root cause.

5. For types whose inner fields already implement Elicitation, delegate:

impl Elicitation for TowerTimeoutLayer {
    type Style = TowerTimeoutLayerStyle;

    async fn elicit<C: ElicitCommunicator>(communicator: &C) -> ElicitResult<Self> {
        let timeout_millis = u64::elicit(communicator).await?;
        Ok(Self { timeout_millis })
    }

    fn kani_proof() -> proc_macro2::TokenStream {
        <u64 as Elicitation>::kani_proof()
    }
    fn verus_proof() -> proc_macro2::TokenStream {
        <u64 as Elicitation>::verus_proof()
    }
    fn creusot_proof() -> proc_macro2::TokenStream {
        <u64 as Elicitation>::creusot_proof()
    }
}

For single-field String types, delegate all three proofs to <String as Elicitation>.

6. ToCodeLiteral is always derived, never written manually.

#[derive(elicitation_derive::ToCodeLiteral)] recovers the exact Rust source expression that creates the descriptor. For TowerTimeoutLayer { timeout_millis: 5000 }, recovery produces TowerTimeoutLayer { timeout_millis: 5000u64 }. This is auditable: trace from any stored value back to the Rust that created it.

3E.3 Inline variant enum for builder-style composition

When a plugin needs to compose multiple layer types into a pipeline (e.g. ServiceBuilder), define a FooLayerKind enum that stores each variant's config inline:

/// Inline config enum — stores each layer variant's config inline (no UUID indirection).
#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize,
    schemars::JsonSchema, elicitation_derive::ToCodeLiteral)]
#[serde(tag = "kind", rename_all = "snake_case")]
pub enum TowerLayerKind {
    Timeout(TowerTimeoutLayer),
    RateLimit(TowerRateLimitLayer),
    MapErr(TowerMapErrLayer),
    // ...
}

Use #[serde(tag = "kind", rename_all = "snake_case")] for JSON discrimination. Never use UUID references for inline composition — that would require shared state between plugins.

3E.4 Plugin structure

Each plugin module follows this pattern (see crates/elicit_tower/src/limit.rs):

// 1. Context type — UUID-keyed registry per descriptor type
pub struct TowerXCtx {
    items: Mutex<HashMap<Uuid, TowerXLayer>>,
}

// 2. Proposition types — one per observable post-condition
pub struct TowerXConfigured;
impl Prop for TowerXConfigured {}
impl VerifiedWorkflow for TowerXConfigured {}

// 3. Tool functions — one per operation (create / describe / emit / list)
#[elicit_tool(plugin = "tower_x", name = "tower_x__new", description = "...", emit = Auto)]
async fn tower_x_new(ctx: Arc<TowerXCtx>, p: TowerXNewParams)
    -> Result<CallToolResult, ErrorData>
{
    let layer = TowerXLayer { timeout_millis: p.timeout_millis };
    let id = Uuid::new_v4();
    ctx.items.lock().await.insert(id, layer);
    let _proof: Established<TowerXConfigured> = Established::assert();
    Ok(json_result(&TowerXIdResult { x_id: id.to_string() }))
}

// 4. Plugin struct — iterates inventory for list_tools / call_tool
pub struct TowerXPlugin(Arc<TowerXCtx>);
impl ElicitPlugin for TowerXPlugin { /* standard inventory dispatch */ }

Standard tool set per descriptor type:

Tool Returns Purpose
foo_x__new { x_id } Create descriptor, store in registry
foo_x__describe JSON of descriptor Inspect stored config
foo_x__emit Rust source string Recover Rust code that creates this config
foo_x__list [{ x_id, … }] List all stored descriptors

3E.5 EmitCode for closure/expression fields

When a descriptor has a body: String or mapper_fn: String field, the plugin's EmitCode impl parses it and splices it into quote!:

fn parse_expr(s: &str) -> proc_macro2::TokenStream {
    s.parse().unwrap_or_else(|_| {
        let lit = s;
        quote::quote! { compile_error!(#lit) }
    })
}

impl EmitCode for TowerMapErrLayerEmit {
    fn emit_code(&self) -> proc_macro2::TokenStream {
        let mapper = parse_expr(&self.0.mapper_fn);
        quote::quote! { tower::util::MapErrLayer::new(#mapper) }
    }
}

This is identical to how elicit_tokio handles SpawnParams { body: String }.

3E.6 Trenchcoat pattern

When a third-party type needs Serialize + Deserialize + JsonSchema but cannot derive them (e.g. it contains non-serializable fields, or it is #[non_exhaustive]), use a trenchcoat — a newtype wrapper that derives the needed traits:

/// Trenchcoat for `foo::ComplexType` — derives serde/JsonSchema for MCP transport.
#[derive(Debug, Clone, serde::Serialize, serde::Deserialize, schemars::JsonSchema)]
pub struct FooComplexTypeWrapper {
    pub field_a: String,
    pub field_b: u32,
}

// From impls bridge between wrapper and original:
impl From<FooComplexTypeWrapper> for foo::ComplexType { /* ... */ }
impl From<foo::ComplexType> for FooComplexTypeWrapper { /* ... */ }

The wrapper is the descriptor — the original type is never exposed directly over MCP.

3E.7 Reference implementation

crates/elicit_tower/ — 7 plugins, 72 MCP tools:

  • limit.rs — ConcurrencyLimitLayer, RateLimitLayer, LoadShedLayer, SpawnReadyLayer
  • retry.rs — RetryLayer, ExponentialBackoffMaker, TpsBudget
  • http.rs — 14 tower-http layers
  • util.rs — MapErrLayer, MapRequestLayer, MapResponseLayer, MapResultLayer, AndThenLayer, ThenLayer, BoxServiceConfig, BoxCloneServiceConfig
  • builder.rs — TowerLayerKind inline enum + ServiceBuilder descriptor
  • balance.rs — Balance, PeakEwma, PendingRequests
  • steer.rs — Steer

Phase 3F — Factory Pattern for Generic APIs

Use this phase when a third-party API is parameterized by a user type — Router<S>, Json<T>, State<S>, Extension<T> — and the tools must be specialized per concrete type.

3F.1 When to use

  • The API type Foo<T> requires T to implement a trait (e.g. Clone + Send + Sync)
  • Different users of your crate will supply different T types
  • The tool schema and behavior differ per T (field names, validation, etc.)
  • T is always ElicitComplete — the factory constraint guarantees all trait machinery

3F.2 Pattern

The plugin exposes a builder that the downstream crate calls at startup, registering each concrete T:

pub struct AxumRouterPlugin {
    tools: Vec<Box<dyn ElicitPlugin>>,
}

impl AxumRouterPlugin {
    pub fn builder() -> AxumRouterPluginBuilder { AxumRouterPluginBuilder::default() }
}

pub struct AxumRouterPluginBuilder { /* ... */ }

impl AxumRouterPluginBuilder {
    /// Register a concrete state type S for Router<S> tools.
    /// Requires S: ElicitComplete — the compiler enforces all trait machinery.
    pub fn register_state<S: ElicitComplete + 'static>(
        mut self,
        name: &'static str,
        description: &'static str,
    ) -> Self {
        // Generates tools: axum_router__{name}__new, __route, __layer, __emit, etc.
        self.registrations.push(Box::new(AxumRouterRegistration::<S>::new(name, description)));
        self
    }

    pub fn build(self) -> AxumRouterPlugin { AxumRouterPlugin { tools: self.registrations } }
}

Downstream integration code:

let router_plugin = AxumRouterPlugin::builder()
    .register_state::<AppState>("app_state", "Main application state")
    .build();

This generates tools at runtime:

  • axum_router__app_state__new
  • axum_router__app_state__route
  • axum_router__app_state__layer
  • axum_router__app_state__emit

3F.3 Tool naming convention

{plugin}__{type_name}__{action} — all lowercase, double-underscore separators.

The type_name is the caller-supplied registration name ("app_state"), not the Rust type name. This keeps tool names stable across refactors.

3F.4 ElicitComplete as the factory constraint

Always bound generic type parameters with ElicitComplete:

pub fn register_state<S: ElicitComplete + 'static>(/* ... */) -> Self

ElicitComplete is a supertrait of Elicitation + ElicitIntrospect + ElicitSpec + Serialize + Deserialize + JsonSchema. Using it as the bound means the compiler rejects any S that is missing any piece of the framework — no runtime surprises.

3F.5 Reference

crates/elicit_tokio/src/spawn.rs — TokioSpawnPlugin::builder() with register_blocking::<T>() and register_async::<T>() is the canonical example of the factory pattern.

3F.6 Multi-Parameter Factory

When the core type has multiple independent generic parameters — Foo<A, B, C> — the factory pattern extends naturally. Each parameter that is ElicitComplete contributes independently to tool naming, schema, and code generation.

When to use

  • The API type has ≥2 independent generics (e.g. Quantity<D, U, V>, HashMap<K, V>)
  • Each parameter is a distinct semantic axis (dimension vs unit system vs value type)
  • Parameters can meaningfully vary independently — different registrations explore the product space

Canonical example: uom::Quantity<D, U, V>

uom represents physical quantities as Quantity<D, U, V> where:

  • D: Dimension — type-level dimensional powers (Length, Mass, Velocity, …)
  • U: Units<V> — unit system (SI, CGS, …)
  • V: Num + Conversion<V> — underlying storage (f64, f32, i32, …)

In practice, uom exposes convenient type aliases (uom::si::f64::Length, uom::si::f64::Mass) which are fully-specialized instantiations of the 3-parameter generic. The factory registers these concrete type aliases — one type parameter at the call site that resolves to three:

pub struct UomQuantityPlugin { /* ... */ }
impl UomQuantityPlugin {
    pub fn builder() -> UomQuantityPluginBuilder { Default::default() }
}

impl UomQuantityPluginBuilder {
    /// Register a concrete quantity type Q (e.g. uom::si::f64::Length).
    /// Q must be Quantity<D, U, V> for some D, U, V — the factory monomorphizes
    /// tools for this exact (D, U, V) triple.
    ///
    /// `name` is the caller-supplied namespace for generated tools:
    /// `{name}__new`, `{name}__get`, `{name}__add`, `{name}__emit`, etc.
    pub fn register_quantity<Q>(mut self, name: &'static str) -> Self
    where
        Q: QuantityElicit + 'static,  // supertrait: Quantity + ElicitComplete
    {
        self.registrations.push(Box::new(QuantityRegistration::<Q>::new(name)));
        self
    }
}

Downstream usage:

let plugin = UomQuantityPlugin::builder()
    .register_quantity::<uom::si::f64::Length>("length")
    .register_quantity::<uom::si::f64::Mass>("mass")
    .register_quantity::<uom::si::f64::Time>("time")
    .register_quantity::<uom::si::f64::Velocity>("velocity")
    .build();
// Generates: length__new, length__get, length__add, length__emit,
//            mass__new, mass__get, mass__add, mass__emit, ...

Each registration gets its own typed HashMap<Uuid, Q> — no enum-wrapper, no type erasure. The compiler knows the exact type at codegen time.

The ElicitComplete advantage for multi-param factories

When each dimension parameter is independently ElicitComplete:

// Each of D, U, V contributes to code emission independently:
// D knows: "I am Length; my SI unit is meter; I accept foot, km, ..."
// U knows: "I am the SI system; I emit as uom::si::SI"
// V knows: "I am f64; I emit as f64"

// Factory can compose these to generate:
// "use uom::si::f64::Length; let x = Length::new::<meter>(5.0);"

This compositional code generation is the unique value of multi-param ElicitComplete over a single opaque concrete type. Each parameter's EmitCode impl produces a fragment; the factory combines them into dimension-correct, unit-safe Rust source.

Cross-registration arithmetic: the QuantityBus

Multi-registration creates a coordination challenge: length_id / time_id = velocity_id spans three different typed HashMaps. The solution is a QuantityBus — a shared routing layer all registrations contribute to.

/// Shared bus: maps UUID → (quantity_name, f64_in_si_base_units).
/// Allows cross-registration arithmetic without type erasure of the primary storage.
pub type QuantityBus = Arc<Mutex<HashMap<Uuid, QuantityBusEntry>>>;

pub struct QuantityBusEntry {
    pub name: &'static str,   // "length", "mass", etc. — registration name
    pub si_value: f64,        // always in SI base units
}

Each {name}__new tool writes to both the typed HashMap (for emission, type-safe ops) and the QuantityBus (for cross-type ops). The bus-level arithmetic tool (qty__div, qty__mul) reads SI values from the bus, computes, resolves the result dimension from the derivation table, and routes the result into the appropriate typed HashMap.

length_id  ──bus──> 30.48 m           }
time_id    ──bus──> 9.58 s            } qty__div resolves → Velocity
                                       } creates velocity_id in velocity HashMap
                                       } writes velocity_id + 3.18 m/s to bus

Both storage layers coexist:

  • Typed HashMap — used by {name}__emit (knows the uom type, emits perfect code)
  • QuantityBus — used by cross-type arithmetic (works on f64 SI values)

Naming convention

{registration_name}__{action} — all lowercase, double-underscore.

With multi-param factory the registration name encodes all parameters that matter to users: "length_cgs_f32" for CGS f32 Length, "length" for the common SI f64 case.

When NOT to use multi-param factory

  • Parameters are not independently meaningful to callers (use a single opaque type)
  • The product space is fixed and small (use the enum-wrapper runtime pattern instead — simpler, no QuantityBus needed)
  • Cross-registration arithmetic is the primary operation (bus overhead dominates)

4.1 Cargo.toml

[dependencies]
foo = { workspace = true, optional = true }

[features]
foo-types = ["dep:foo", "elicitation/foo-types"]

4.2 Proof file src/foo_types.rs

For Select enum types — verify the three invariants the MCP machinery depends on:

//! Kani proofs for foo type elicitation.

#[cfg(feature = "foo-types")]
use elicitation::Select;

// Label count: labels().len() == options().len()
#[cfg(feature = "foo-types")]
#[kani::proof]
fn verify_my_enum_label_count() {
    let labels = foo::MyEnum::labels();
    let options = foo::MyEnum::options();
    assert!(labels.len() == options.len(), "labels and options have equal length");
    assert!(labels.len() == N, "MyEnum has N variants");
}

// Full roundtrip: every label is accepted by from_label()
#[cfg(feature = "foo-types")]
#[kani::proof]
fn verify_my_enum_all_labels_roundtrip() {
    let labels = foo::MyEnum::labels();
    for label in &labels {
        let result = foo::MyEnum::from_label(label);
        assert!(result.is_some(), "MyEnum label roundtrips");
    }
}

// Unknown rejection
#[cfg(feature = "foo-types")]
#[kani::proof]
fn verify_my_enum_unknown_rejected() {
    let result = foo::MyEnum::from_label("__unknown__");
    assert!(result.is_none(), "MyEnum rejects unknown labels");
}

For third-party struct/builder types — explicit trusted assumption:

#[cfg(feature = "foo-types")]
#[kani::proof]
fn verify_foo_my_builder_trusted_third_party() {
    // foo::MyBuilder is a third-party type from the foo crate.
    // We trust its construction invariants are upheld by the foo library.
    // Our Elicitation impl only adds interactive prompting behavior.
    kani::assume(true);
}

4.3 Wire in src/lib.rs

#[cfg(all(kani, feature = "foo-types"))]
mod foo_types;

4.4 Register in ProofHarness::all() (src/verification/runner.rs in elicitation)

// foo_types
Self::new("foo_types", "verify_my_enum_label_count"),
Self::new("foo_types", "verify_my_enum_all_labels_roundtrip"),
Self::new("foo_types", "verify_my_enum_unknown_rejected"),
Self::new("foo_types", "verify_foo_my_builder_trusted_third_party"),

4.5 Run the proofs — verify they pass

Do not skip this step. cargo check only confirms compilation; it does not run the model checker. Unrun proofs are not verified proofs.

# Smoke-test one harness first to confirm it doesn't hang or fail
cargo kani --harness verify_my_enum_label_count \
    -p elicitation_kani --all-features --default-unwind 20

# Then run all foo_types harnesses via the tracker (writes kani_verification_results.csv)
just verify-kani-tracked

Expected output for each harness: VERIFICATION:- SUCCESSFUL. Any FAILED or timeout means the proof code needs fixing before committing.

The CSV (kani_verification_results.csv) is a local artifact — it is gitignored and regenerated by just verify-kani-tracked. Do not commit it.

Phase 5 — Creusot Verification (crates/elicitation_creusot/)

5.1 Cargo.toml

[dependencies]
foo = { workspace = true, optional = true }

[features]
foo-types = ["dep:foo", "elicitation/foo-types"]

5.2 Proof file src/foo_types.rs

Creusot uses #[requires]/#[ensures]/#[trusted] from creusot-std. For types we cannot symbolically execute (all third-party types), use #[trusted]. The label count proof is the one exception — it can be de-trusted after adding extern_specs (see §5.4).

//! Creusot proofs for foo type elicitation.

#![cfg(feature = "foo-types")]

use creusot_std::prelude::*;
use elicitation::Select;

/// Verify MyEnum label count equals option count.
///
/// De-trusted: Alt-Ergo discharges this after extern_spec axioms supply the
/// concrete lengths. See extern_specs.rs §5.4.
#[requires(true)]
#[ensures(result == true)]
pub fn verify_my_enum_label_count() -> bool {
    foo::MyEnum::labels().len() == foo::MyEnum::options().len()
}

/// Verify MyEnum from_label returns Some for a known valid label.
#[requires(true)]
#[ensures(result == true)]
#[trusted]
pub fn verify_my_enum_known_label_accepted() -> bool {
    let labels = foo::MyEnum::labels();
    !labels.is_empty() && foo::MyEnum::from_label(&labels[0]).is_some()
}

/// Verify MyEnum from_label returns None for an unknown label.
#[requires(true)]
#[ensures(result == true)]
#[trusted]
pub fn verify_my_enum_unknown_label_rejected() -> bool {
    foo::MyEnum::from_label("__unknown__").is_none()
}

/// Trust axiom: foo::MyBuilder invariants are maintained by the foo crate.
#[requires(true)]
#[ensures(result == true)]
#[trusted]
pub fn verify_foo_builder_trusted() -> bool {
    true
}

5.3 Wire in src/lib.rs

Both mod and pub use are required — all other feature-gated modules export their proof functions at the crate root for discoverability.

#[cfg(feature = "foo-types")]
mod foo_types;

#[cfg(feature = "foo-types")]
pub use foo_types::*;

5.4 Add extern_spec axioms for label count de-trusting

The verify_my_enum_label_count() proof above has no #[trusted], so Alt-Ergo must discharge the len() == len() goal. Without axioms, labels() and options() are opaque program functions and the goal is unprovable.

Add extern_spec! blocks in extern_specs.rs stating the concrete variant count:

// extern_specs.rs — bottom of file, gated on the same feature

#[cfg(feature = "foo-types")]
extern_spec! {
    impl elicitation::Select for foo::MyEnum {
        #[ensures(result@.len() == N)]   // N = number of variants
        fn labels() -> Vec<String>;

        #[ensures(result@.len() == N)]
        fn options() -> Vec<foo::MyEnum>;
    }
}

Repeat for each Select enum in the crate. Count variants by inspecting the Select impl's from_label match arms in src/primitives/foo_types/.

5.5 Register in CreusotModule::all() (src/verification/creusot_runner.rs in elicitation)

Self::with_feature("foo_types", "foo-types"),

5.6 Run the proofs — verify they pass

Do not skip this step. cargo check only confirms compilation; it does not discharge any proof obligations. Unproved goals are not verified proofs.

# Step 1: regenerate .coma WhyML files
cargo creusot -- -p elicitation_creusot --features foo-types

# Step 2: confirm .coma files were generated for de-trusted proofs
ls verif/elicitation_creusot_rlib/foo_types/

# Step 3: prove each de-trusted goal
cargo creusot prove \
    "verif/elicitation_creusot_rlib/foo_types/verify_my_enum_label_count.coma" \
    -- -p elicitation_creusot --features foo-types

Expected output: Library verif.elicitation_creusot_rlib.foo_types.verify_my_enum_label_count.Coma: ✔

Any ✘ means either the extern_spec variant count is wrong or the proof body is incorrect. #[trusted] proofs generate no .coma files — only de-trusted proofs do.

Phase 6 — Verus Verification (crates/elicitation_verus/)

6.1 Cargo.toml

Verus does not use workspace deps the same way — check existing patterns in the crate.

6.2 Proof file src/foo_types.rs (added to external_types.rs or new file)

Verus proofs are written inside verus! { ... } blocks and use abstract boolean parameters to represent third-party state that cannot be symbolically computed:

use verus_builtin_macros::verus;

verus! {

// ============================================================================
// foo crate types
// ============================================================================

/// Proof that MyEnum from_label succeeds for a known valid label.
pub fn verify_my_enum_label_roundtrip(label_is_known: bool) -> (result: bool)
    ensures result == label_is_known,
{
    label_is_known
}

/// Proof that MyEnum rejects unknown labels.
pub fn verify_my_enum_unknown_rejected(label_is_unknown: bool) -> (result: bool)
    ensures result == label_is_unknown,
{
    label_is_unknown
}

/// Trust axiom: foo::MyBuilder is a trusted third-party type.
pub fn verify_foo_builder_trusted() -> (result: bool)
    ensures result == true,
{
    true
}

} // verus!

6.3 Wire in src/lib.rs

pub mod foo_types;

6.4 Register in VerusProof::all() (src/verification/verus_runner.rs in elicitation)

Add one entry per proof function:

// foo_types (N proofs)
Self::new("foo_types", "verify_my_enum_label_roundtrip"),
Self::new("foo_types", "verify_my_enum_unknown_rejected"),
Self::new("foo_types", "verify_foo_builder_trusted"),

6.5 Run the proofs — verify they pass

Do not skip this step. cargo check does not run Verus. The verifier must be invoked explicitly; an unrun proof is not a verified proof.

# Run Verus directly on the new module (fast, isolated)
verus --crate-type=lib crates/elicitation_verus/src/foo_types.rs

Expected: verification results:: N verified, 0 errors

Any errors mean the ensures/requires contracts or the proof body need fixing. Once all proofs pass, the tracker (just verify-verus-tracked) picks them up via VerusProof::all().

Phase 7 — ElicitComplete Registration and Proof Validation

This is the final phase for every new type. It sews up the implementation, lets the compiler enforce the growing checklist of framework traits, and ensures the proof composition guarantee is upheld.

7.1 Implement ElicitComplete

Add a blanket or explicit impl ElicitComplete for your type. The compiler will reject it if any supertrait obligation is missing — this is the enforced checklist:

// In crates/elicitation/src/primitives/foo_types/bar.rs
impl ElicitComplete for Bar {}

ElicitComplete requires:

  • Elicitation — with non-defaulted kani_proof, verus_proof, creusot_proof
  • ElicitIntrospect — structural metadata
  • ElicitSpec — agent-browsable contract spec
  • serde::Serialize + for<'de> serde::Deserialize<'de> — data interchange
  • schemars::JsonSchema — JSON schema generation

If the compiler rejects the impl, you have missed something from the earlier phases. Use the error messages as your gap finder — do not paper over them with #[allow].

7.2 Add to proof_non_empty_test.rs

Open crates/elicitation/tests/proof_non_empty_test.rs and add your type to the appropriate test. This verifies that none of the three proof methods return an empty TokenStream:

#[test]
fn bar_proofs_non_empty() {
    assert_proofs_non_empty::<Bar>("Bar");
    assert_proofs_non_empty::<BarWrapper>("BarWrapper"); // add wrappers too
}

The test uses validate_proofs_non_empty() from ElicitComplete, which checks all three systems at once.

7.3 Add to proof_composition_test.rs (aggregate types only)

If your type is an aggregate (has fields of other Elicitation types), add containment assertions to crates/elicitation/tests/proof_composition_test.rs:

#[test]
fn bar_delegates_to_constituents() {
    // Bar { inner: Baz, count: u32 }
    assert_kani_contains::<Bar, Baz>("Bar contains Baz proof");
    assert_kani_contains::<Bar, u32>("Bar contains u32 proof");
}

This catches regressions where a refactor drops a delegation call from the manually-written proof body.

Note: Types derived with #[derive(Elicit)] do not need composition tests — the macro generates delegation mechanically from the struct fields. Composition tests are only needed for manual impl Elicitation blocks.

7.4 Run tests

just test-package elicitation

All new tests must pass. Zero failures, zero compilation errors.

7.5 Commit

git commit -m "feat(foo-types): register ElicitComplete and add proof validation tests"

Phase 8 — VerifiedWorkflow Registration and Proof Validation

This is the final phase for workflow proposition types — the typestate markers used in Established<P> contracts. It mirrors Phase 7 for elicitation core types.

When to use this phase

Apply Phase 8 whenever you add proposition (Prop) types to a workflow crate (e.g. elicit_foo/src/workflow.rs). If your crate has no workflow plugin, skip this phase entirely.

8.1 Define the proposition

For a zero-cost typestate marker, use #[derive(Prop)]:

/// Proposition: the input was successfully validated.
#[derive(Prop)]
pub struct FooValidated;

For a proposition with meaningful semantic content, write a manual impl Prop:

impl Prop for FooValidated {
    #[cfg(feature = "proofs")]
    fn kani_proof() -> elicitation::proc_macro2::TokenStream {
        quote::quote! {
            #[kani::proof]
            fn verify_foo_validated_axiom() { /* ... */ }
        }
    }
    // verus_proof and creusot_proof similarly
}

Use #[derive(Prop)] for simple marker types — it generates uniquely-named trivial harnesses for all three verifiers automatically.

8.2 Register VerifiedWorkflow

Add the impl immediately after the Prop impl:

impl VerifiedWorkflow for FooValidated {}

The compiler accepts this only when FooValidated: Prop with all three proof methods present. If the #[derive(Prop)] or manual impl Prop is missing or incomplete, the compiler will reject with a precise error.

8.3 Add to workflow_verified_test.rs

Create or open crates/elicit_foo/tests/workflow_verified_test.rs:

#![cfg(feature = "proofs")]

use elicit_foo::FooValidated;
use elicitation::VerifiedWorkflow;

#[track_caller]
fn assert_verified<T: VerifiedWorkflow>(label: &str) {
    assert!(T::validate_proofs_non_empty(), "{label}: proofs are empty");
}

#[test]
fn foo_props_non_empty() {
    assert_verified::<FooValidated>("FooValidated");
}

8.4 Add composition tests (composite And<P, Q> only)

If your workflow exposes a production composite type (e.g. And<UrlParsed, HttpsRequired>), add containment assertions to the same test file:

#[test]
fn foo_and_contains_constituents() {
    use elicitation::contracts::And;
    type Composite = And<FooValidated, FooAuthorized>;
    assert!(Composite::kani_proof_contains::<FooValidated>());
    assert!(Composite::kani_proof_contains::<FooAuthorized>());
}

Composition tests are only needed for manual impl Prop blocks or explicitly documented composite types. And<P, Q> propagates mechanically — the blanket impl in VerifiedWorkflow guarantees delegation without additional test coverage.

8.5 Run and commit

just test-package elicit_foo --features proofs
git commit -m "feat(elicit-foo): register VerifiedWorkflow and add proof validation tests"

Checklist Summary

Use this to track progress when adding a new crate:

Crate: foo
Feature flag: foo-types

[ ] Workspace Cargo.toml: dep + member added
[ ] elicitation/Cargo.toml: optional dep + feature flag
[ ] elicitation/src/primitives/foo_types/ directory created
[ ] Each type file: Prompt + Select (or text) + Elicitation + ElicitIntrospect
[ ] primitives/mod.rs: mod foo_types gated
[ ] lib.rs: pub use exports gated
[ ] type_spec/foo_specs.rs: ElicitSpec impls (impl_select_spec! / impl_builder_spec!)
[ ] type_spec/mod.rs: mod foo_specs added
[ ] just check-all elicitation passes clean

[ ] elicit_foo/Cargo.toml created
[ ] elicit_foo/src/lib.rs created (mod + pub use only)
[ ] Each type file: elicit_newtype! + elicit_newtype_traits! + #[reflect_methods]
[ ] Workspace wired (members + workspace.dependencies)
[ ] just check-all elicit_foo passes clean

(Optional — if the crate exposes derive traits worth wrapping as MCP tools:)
[ ] elicit_foo/Cargo.toml: add elicitation_macros + inventory + serde_json deps
[ ] For each foreign type used as a param/return: add From<Wrapper> for Original impl
[ ] elicit_foo/src/trait_factories.rs: #[reflect_trait] for each trait
[ ] Startup docs updated with prime_foo__trait_name::<T>() + register_type::<T>() pattern
[ ] elicit_foo/tests/trait_factories_test.rs: inventory + lifecycle + invocation tests

[ ] elicitation_kani/Cargo.toml: dep + feature
[ ] elicitation_kani/src/foo_types.rs: proof harnesses
[ ] elicitation_kani/src/lib.rs: mod foo_types gated
[ ] verification/runner.rs: ProofHarness::all() entries added
[ ] Select enums: label_count + all_labels_roundtrip + unknown_rejected proofs
[ ] Struct/builder types: trusted_third_party kani::assume(true) proofs
[ ] cargo kani --harness verify_... -p elicitation_kani --all-features --default-unwind 20 passes (smoke test)
[ ] just verify-kani-tracked — all new harnesses show SUCCESSFUL in CSV

[ ] elicitation_creusot/Cargo.toml: dep + feature
[ ] elicitation_creusot/src/foo_types.rs: proof functions
[ ] elicitation_creusot/src/lib.rs: mod foo_types AND pub use foo_types::* (both required)
[ ] extern_specs.rs: extern_spec! blocks for each Select enum label count (N variants)
[ ] Label count proofs: #[trusted] removed (de-trusted via extern_specs)
[ ] All other proofs: #[trusted] retained (string literal opacity wall)
[ ] creusot_runner.rs: CreusotModule::all() entry added (Self::with_feature("foo_types", "foo-types"))
[ ] cargo creusot -- -p elicitation_creusot --features foo-types compiles (generates .coma)
[ ] cargo creusot prove "verif/.../foo_types/verify_*_label_count.coma" — all return ✔

[ ] elicitation_verus/src/foo_types.rs: verus! block
[ ] elicitation_verus/src/lib.rs: pub mod foo_types
[ ] verus_runner.rs: VerusProof::all() entries added (one per proof function)
[ ] verus --crate-type=lib crates/elicitation_verus/src/foo_types.rs → N verified, 0 errors

[ ] impl ElicitComplete for each new type (compiler enforces all supertrait gaps)
[ ] proof_non_empty_test.rs: assert_proofs_non_empty::<Foo> for each new type + wrappers
[ ] proof_composition_test.rs: assert_kani_contains for aggregate types with manual impls
[ ] just test-package elicitation passes clean

(If the crate has a workflow plugin with Prop types:)
[ ] #[derive(Prop)] or manual impl Prop for each proposition type
[ ] impl VerifiedWorkflow for each proposition type (compiler enforces Prop completeness)
[ ] tests/workflow_verified_test.rs: assert_verified for each Prop + And<P,Q> containment
[ ] just test-package elicit_foo --features proofs passes clean

[ ] git commit -m "feat(foo-types): add Elicitation + verification support for foo crate"
[ ] git push

For macro / fragment-only crates (skip Phases 2, 4, 5, 6):

Crate: foo_macros
(no feature flag needed — no elicitation primitives)

[ ] Workspace Cargo.toml: member added
[ ] elicit_foo/Cargo.toml: elicitation (features=["emit"]), proc-macro2, quote, inventory
[ ] For each macro:
    [ ] src/my_macro.rs: params struct (Deserialize + JsonSchema)
    [ ] CustomEmit<P> type: impl CustomEmit<MyMacroParams> with emit_code() + quote!
    [ ] EmitEntry newtype + impl EmitCode (thin wrapper calling CustomEmit::emit_code)
    [ ] inventory::submit!(EmitEntry { tool, crate_name, constructor })
[ ] src/plugin.rs: #[derive(ElicitPlugin)] + #[elicit_tool(emit = MyMacroEmit)] handlers
    (handler returns MyMacroEmit::emit_code(&p).to_string() — does NOT call p.emit_code())
[ ] src/lib.rs: mod + pub use only
[ ] just check-all elicit_foo passes clean

[ ] Assemble: use shared std__assemble or add domain-specific terminal tool
    (see Fragment Tools section — no separate assemble needed for most crates)

[ ] tests/macro_tools_test.rs: EmitCode output, serde roundtrip, dispatch_emit_from, fragment composition

[ ] git commit -m "feat(elicit_foo): fragment tools for foo macros"
[ ] git push

Type Category Reference

The decision of what to verify follows directly from the core principle: we own the from_label/Elicitation logic — verify that. We don't own the variant definitions — trust those.

Type shape Elicitation pattern What we verify What we trust
Enum with known variants Select from_label roundtrip + unknown rejection Variant definitions from upstream
#[non_exhaustive] enum Select + wildcard _ => Same roundtrip invariants on our labels Any new variants added by upstream
Newtype around String/primitive text + T::new(s) Our parse/construction path Inner type's own invariants
Builder struct text prompt + builder API kani::assume(true) — trust upstream entirely All builder invariants
Complex owned struct Survey (multi-field) kani::assume(true) — trust upstream entirely All struct invariants
Third-party derive trait #[reflect_trait] factory Inventory registration + prime/instantiate lifecycle Trait method implementations in upstream
Config/layer descriptor (Phase 3E) ToCodeLiteral + UUID registry kani::assume(true) — value is in code recovery All runtime type invariants
Fn/closure/expression field body: String or mapper_fn: String No runtime verification — From impl omitted Closure correctness (agent-supplied source)
Generic Foo<T> where T: ElicitComplete Factory pattern (Phase 3F) Per-type tool generation + compiler-enforced T: ElicitComplete T's own trait impls

Fragment Tools (Macros and Closures)

Some Rust APIs are macros or closures that execute at compile time or as runtime callbacks, and cannot be called directly through an MCP boundary. Use the fragment tool pattern for these.

Two tool kinds

Kind Returns Composable? EmitEntry?
Fragment tool TokenStream as string ✅ Pass to other tools ✅ Yes
Terminal tool (assemble) { main_rs, cargo_toml } ❌ Final step only ❌ No

When to use fragment tools

Use this pattern when:

  • The API is a Rust macro (format!, query!, include_str!, etc.)
  • The API generates code, not runtime data
  • The fragment may be composed with other fragments before assembly

Fragment composition model

Fragment tools produce TokenStream strings that can be chained:

  • Expression-level nesting: pass a fragment as an arg/field to another tool
  • Statement-level assembly: collect fragments as steps in std__assemble
std__env { var: "USER" }               →  env!("USER")
                                              ↓ pass as arg
std__format { template: "Hi, {}!", args: ["env!(\"USER\")"] }
                                       →  format!("Hi, {}!", env!("USER"))
                                              ↓ wrap as statement + pass to
std__assemble { steps: ["let msg = format!(...); println!(\"{}\", msg);"] }
                                       →  { main_rs, cargo_toml }

Implementation checklist — Fragment tool

1. Params struct (in crates/elicit_foo/src/my_macro.rs):

#[derive(Debug, Clone, Serialize, Deserialize, JsonSchema)]
pub struct MyMacroParams {
    pub arg: String,
}

Do not write impl EmitCode for MyMacroParams — the #[elicit_tool] macro generates EmitCode automatically from the emit = MyMacroEmit attribute.

2. Custom emit type (co-located with the params struct):

use elicitation::emit_code::CustomEmit;

pub struct MyMacroEmit;
impl CustomEmit<MyMacroParams> for MyMacroEmit {
    fn emit_code(p: &MyMacroParams) -> TokenStream {
        let arg = &p.arg;
        quote! { my_macro!(#arg) }
    }
}

3. EmitEntry inventory — still needed for N→1 binary recovery via emit_dispatch_crate:

use elicitation::emit_code::{CrateDep, EmitCode, EmitEntry};

struct MyMacroEmitEntry(MyMacroParams);
impl EmitCode for MyMacroEmitEntry {
    fn emit_code(&self) -> TokenStream { MyMacroEmit::emit_code(&self.0) }
    fn crate_deps(&self) -> Vec<CrateDep> {
        vec![CrateDep { name: "my_crate", version: "1", features: &[] }]
    }
}

inventory::submit! {
    EmitEntry {
        tool: "foo__my_macro",
        crate_name: "elicit_foo",
        constructor: |v| {
            serde_json::from_value::<MyMacroParams>(v)
                .map(|p| Box::new(MyMacroEmitEntry(p)) as Box<dyn EmitCode>)
                .map_err(|e| e.to_string())
        },
    }
}

4. Handler (in crates/elicit_foo/src/plugin.rs) — performs the runtime work and returns the code fragment as text. Do not call p.emit_code() inside the handler body; that is the macro's responsibility:

#[elicit_tool(
    plugin = "foo",
    name = "foo__my_macro",
    description = "Emit a my_macro!(…) expression as a Rust source fragment. \
                   Pass the returned string as an expression to another tool, \
                   or collect as a step for std__assemble.",
    emit = MyMacroEmit
)]
#[instrument(skip_all)]
async fn emit_my_macro(p: MyMacroParams) -> Result<CallToolResult, ErrorData> {
    // Compute the fragment at runtime and return it as text to the agent.
    let source = MyMacroEmit::emit_code(&p).to_string();
    Ok(CallToolResult::success(vec![Content::text(source)]))
}

5. Cargo.toml — add emit feature to elicitation dep:

elicitation = { workspace = true, features = ["emit"] }
proc-macro2.workspace = true
quote.workspace = true
inventory.workspace = true

4. No Phase 2 (elicitation core) — fragment tools do not need Elicit impls in crates/elicitation/src/primitives/. Skip Phase 2 entirely.

5. No Kani/Creusot verification — fragment tools return TokenStream; the verification story is handled when the emitted program is verified, not here.

Implementation checklist — Terminal tool (assemble)

Each macro crate does not need its own assemble tool. The shared std__assemble in elicit_std works for any fragments because it uses RawFragment to re-parse pre-rendered strings:

// AssembleParams wraps each step in RawFragment and passes to BinaryScaffold
let steps: Vec<Box<dyn EmitCode>> = self.steps.iter()
    .map(|s| Box::new(RawFragment(s.clone())) as Box<dyn EmitCode>)
    .collect();
let scaffold = BinaryScaffold::new(steps, self.with_tracing);
let main_rs = scaffold.to_source()?;
let cargo_toml = scaffold.to_cargo_toml(&self.package_name);

If a crate needs a domain-specific assembly tool (e.g. pre-wired use statements or custom error handling), use the same RawFragment pattern. Note: crate deps from raw fragments are NOT automatically detected — callers must ensure the assembled source only uses crates already in the generated Cargo.toml.

Reference implementation

crates/elicit_std — five tools (four fragment, one terminal):

Tool Kind Params
std__format fragment { template, args[] }
std__include_str fragment { path }
std__env fragment { var, error_message? }
std__concat fragment { parts[] }
std__assemble terminal { steps[], with_tracing?, package_name? }

Tests: crates/elicit_std/tests/macro_tools_test.rs (31 tests)

Reference Implementation

The complete clap integration is the canonical example:

Elicitation core:

  • crates/elicitation/src/primitives/clap_types/ — 11 type files
  • Feature flag: clap-types

Wrapper crate (newtypes + trait factories):

  • crates/elicit_clap/src/ — 11 newtype wrapper files + trait_factories.rs
  • crates/elicit_clap/tests/trait_factories_test.rs — 20 integration tests
  • Traits covered: CommandFactory, Subcommand, ValueEnum, Args
  • Traits deferred (incompatible signatures): FromArgMatches, Parser

Verification:

  • crates/elicitation_kani/src/clap_types.rs — 24 proof harnesses
  • crates/elicitation/src/verification/runner.rs — harness registration

Key commits:

  • feat(elicit_clap): add newtype wrappers for clap types with MCP reflect methods
  • feat(elicitation_macros): #[reflect_trait] macro + DynamicToolRegistry
  • feat(elicit_clap): clap trait factories with type_map bridging
  • test(elicit_clap): 20 integration tests for all clap trait factories