lean_host_mcp/
envelope.rs

1//! The uniform response envelope every tool returns.
2//!
3//! Encoding contract (default `quiet` telemetry verbosity):
4//!
5//! ```jsonc
6//! {
7//!   "status": "ok",
8//!   "result":   { /* tool-specific; null for runtime_unavailable */ },
9//!   "runtime_error": null,
10//!   "freshness": {
11//!     "project_root":   "/abs/path",
12//!     "session_id":     "uuid",
13//!     "lean_toolchain": "leanprover/lean4:v4.x.y"
14//!   },
15//!   "warnings":     ["..."],     // omitted when empty
16//!   "next_actions": ["..."]      // omitted when empty
17//! }
18//! ```
19//!
20//! What the model reads is kept to proof-relevant content. Operational
21//! telemetry is gated behind [`TelemetryVerbosity`](crate::tools::TelemetryVerbosity):
22//! in the default `quiet` mode the `runtime` block is omitted unless it carries
23//! an actionable signal (a worker restart — see [`RuntimeFacts::is_actionable`]),
24//! and `freshness` drops `project_hash` (the Lake-manifest SHA-256) and the full
25//! `imports` list. In `full` mode every field is emitted: `runtime` with its
26//! lifecycle/pressure counters, and `freshness` with all five fields, so a
27//! client can branch on `(project_root, project_hash)` to detect dependency
28//! changes between calls.
29//!
30//! Three volatile decisions hide behind one shape: what freshness means,
31//! how it's serialized, and what an MCP "warning" looks like. Tools don't
32//! pick the layout; they build a `Response<T>` and `crate::server` serializes
33//! it after [`Response::trim_telemetry`] applies the verbosity gate.
34
35use std::collections::BTreeMap;
36
37use schemars::JsonSchema;
38use serde::Serialize;
39
40/// The project freshness snapshot a producer builds.
41///
42/// Built by [`crate::project`]'s `freshness` and
43/// [`crate::error::WorkerUnavailable::freshness`]. Not serialized directly:
44/// [`Response::ok`] splits it into the always-emitted [`FreshnessIdentity`] and
45/// the verbosity-gated [`Telemetry`] block.
46#[derive(Debug, Clone)]
47pub struct Freshness {
48    pub project_root: String,
49    pub project_hash: String,
50    pub imports: Vec<String>,
51    pub session_id: String,
52    pub lean_toolchain: String,
53    /// Project-lifetime toolchain-provenance advisories (unknown pin, missing
54    /// provenance sidecar). Carried to the envelope, where one drain
55    /// ([`Response::drain_advisories`], called by [`crate::server`]) moves them
56    /// into the top-level `warnings` array, so "warnings are top-level" holds.
57    pub(crate) toolchain_advisories: Vec<String>,
58}
59
60/// Session identity — always serialized as the envelope's `freshness`.
61///
62/// Small, stable, and occasionally relevant to a proof agent: `session_id`
63/// flips when the worker re-spawns, signalling a context reset.
64#[derive(Debug, Clone, Serialize, JsonSchema)]
65pub struct FreshnessIdentity {
66    pub project_root: String,
67    pub session_id: String,
68    pub lean_toolchain: String,
69}
70
71/// Operational telemetry, serialized as the envelope's `telemetry`.
72///
73/// Emitted only under `full`
74/// [`TelemetryVerbosity`](crate::tools::TelemetryVerbosity). It carries
75/// cache/identity metadata (`project_hash`, the full `imports` list) and the
76/// worker `runtime` facts — none of which a proof agent needs to make progress,
77/// so the default `quiet` mode drops the whole block. The one actionable signal
78/// a restart carries already reaches the agent as a top-level `warning`.
79#[derive(Debug, Clone, Serialize, JsonSchema)]
80pub struct Telemetry {
81    /// Lake-manifest SHA-256. Lets a client branch on `(project_root,
82    /// project_hash)` to detect dependency changes between calls.
83    pub project_hash: String,
84    /// Caller-supplied import set for this session.
85    #[serde(skip_serializing_if = "Vec::is_empty")]
86    pub imports: Vec<String>,
87    /// Worker lifecycle and admission-pressure facts for this call.
88    #[serde(skip_serializing_if = "Option::is_none")]
89    pub runtime: Option<RuntimeFacts>,
90}
91
92#[derive(Debug, Clone, Default, Serialize, JsonSchema)]
93pub struct RuntimeRestartEvent {
94    pub cause: String,
95    pub reason: String,
96    pub worker_generation: u64,
97    pub planned: bool,
98    #[serde(skip_serializing_if = "Option::is_none")]
99    pub rss_kib: Option<u64>,
100    #[serde(skip_serializing_if = "Option::is_none")]
101    pub limit_kib: Option<u64>,
102}
103
104#[derive(Debug, Clone, Default, Serialize, JsonSchema)]
105pub struct RuntimeFacts {
106    pub worker_generation: u64,
107    pub worker_restarted: bool,
108    pub retry_count: u32,
109    pub admission_wait_millis: u64,
110    pub queue_wait_millis: u64,
111    #[serde(skip_serializing_if = "Option::is_none")]
112    pub call_restart: Option<RuntimeRestartEvent>,
113    #[serde(skip_serializing_if = "Option::is_none")]
114    pub last_restart: Option<RuntimeRestartEvent>,
115    #[serde(skip_serializing_if = "Option::is_none")]
116    pub rss_kib: Option<u64>,
117    pub worker_lanes: u32,
118    #[serde(skip_serializing_if = "Option::is_none")]
119    pub import_profile: Option<String>,
120    pub profile_switch_count: u64,
121    /// Worker recycles observed over this project's lifetime, all causes. Lets
122    /// a client see recycle *frequency* (the per-call cause is in `call_restart`).
123    pub restarts_total: u64,
124    /// Lifetime recycle count keyed by stable cause string (e.g. `rss_post_job`).
125    /// Omitted when no recycle has happened.
126    #[serde(skip_serializing_if = "BTreeMap::is_empty")]
127    pub restarts_by_cause: BTreeMap<String, u64>,
128}
129
130#[derive(Debug, Clone, Serialize, JsonSchema)]
131#[serde(rename_all = "snake_case")]
132pub enum ResponseStatus {
133    Ok,
134    RuntimeUnavailable,
135}
136
137#[derive(Debug, Clone, Serialize, JsonSchema)]
138pub struct RuntimeFailure {
139    pub reason: String,
140    pub retryable: bool,
141    pub project_root: String,
142    pub session_id: String,
143    pub worker_generation: u64,
144    pub worker_restarted: bool,
145    #[serde(skip_serializing_if = "Option::is_none")]
146    pub restart_cause: Option<String>,
147    #[serde(skip_serializing_if = "Option::is_none")]
148    pub rss_kib: Option<u64>,
149    #[serde(skip_serializing_if = "Option::is_none")]
150    pub limit_kib: Option<u64>,
151    #[serde(skip_serializing_if = "Option::is_none")]
152    pub retry_after_millis: Option<u64>,
153    #[serde(skip_serializing_if = "Option::is_none")]
154    pub restarts_in_window: Option<u64>,
155    #[serde(skip_serializing_if = "Option::is_none")]
156    pub window_millis: Option<u64>,
157}
158
159#[derive(Debug, Clone, Serialize, JsonSchema)]
160pub struct Response<T>
161where
162    T: Serialize + JsonSchema,
163{
164    pub status: ResponseStatus,
165    pub result: Option<T>,
166    pub runtime_error: Option<RuntimeFailure>,
167    pub freshness: FreshnessIdentity,
168    #[serde(skip_serializing_if = "Option::is_none")]
169    pub telemetry: Option<Telemetry>,
170    #[serde(skip_serializing_if = "Vec::is_empty")]
171    pub warnings: Vec<String>,
172    #[serde(skip_serializing_if = "Vec::is_empty")]
173    pub next_actions: Vec<String>,
174    /// Project-lifetime advisories awaiting the drain into `warnings`. Never
175    /// serialized; emptied by [`Response::drain_advisories`] at the boundary.
176    #[serde(skip)]
177    #[schemars(skip)]
178    pub(crate) advisories: Vec<String>,
179}
180
181/// Split a producer's [`Freshness`] snapshot into the serialized identity, the
182/// telemetry block, and the advisory list the envelope drains into `warnings`.
183fn split_freshness(freshness: Freshness, runtime: Option<RuntimeFacts>) -> (FreshnessIdentity, Telemetry, Vec<String>) {
184    let Freshness {
185        project_root,
186        project_hash,
187        imports,
188        session_id,
189        lean_toolchain,
190        toolchain_advisories,
191    } = freshness;
192    (
193        FreshnessIdentity {
194            project_root,
195            session_id,
196            lean_toolchain,
197        },
198        Telemetry {
199            project_hash,
200            imports,
201            runtime,
202        },
203        toolchain_advisories,
204    )
205}
206
207impl<T> Response<T>
208where
209    T: Serialize + JsonSchema,
210{
211    pub fn ok(result: T, freshness: Freshness) -> Self {
212        let (freshness, telemetry, advisories) = split_freshness(freshness, None);
213        Self {
214            status: ResponseStatus::Ok,
215            result: Some(result),
216            runtime_error: None,
217            freshness,
218            telemetry: Some(telemetry),
219            warnings: Vec::new(),
220            next_actions: Vec::new(),
221            advisories,
222        }
223    }
224
225    pub fn runtime_unavailable(failure: RuntimeFailure, freshness: Freshness, runtime: RuntimeFacts) -> Self {
226        let (freshness, telemetry, advisories) = split_freshness(freshness, Some(runtime));
227        Self {
228            status: ResponseStatus::RuntimeUnavailable,
229            result: None,
230            runtime_error: Some(failure),
231            freshness,
232            telemetry: Some(telemetry),
233            warnings: Vec::new(),
234            next_actions: Vec::new(),
235            advisories,
236        }
237    }
238
239    pub fn result_ref(&self) -> Option<&T> {
240        self.result.as_ref()
241    }
242
243    /// The worker runtime facts, read from the telemetry block. `None` once the
244    /// boundary gate has dropped telemetry (quiet verbosity) or before any
245    /// runtime was attached.
246    pub fn runtime(&self) -> Option<&RuntimeFacts> {
247        self.telemetry.as_ref().and_then(|telemetry| telemetry.runtime.as_ref())
248    }
249
250    /// The caller-supplied import set, read from the telemetry block. Used by
251    /// internal tool composition (e.g. `search_for_proof` reusing a
252    /// `proof_state` response) before the boundary gate runs.
253    pub fn imports(&self) -> &[String] {
254        match &self.telemetry {
255            Some(telemetry) => &telemetry.imports,
256            None => &[],
257        }
258    }
259
260    #[must_use]
261    pub fn with_runtime(mut self, runtime: RuntimeFacts) -> Self {
262        if let Some(telemetry) = self.telemetry.as_mut() {
263            telemetry.runtime = Some(runtime);
264        }
265        self
266    }
267
268    /// Drop the telemetry block — the default `quiet` verbosity gate, applied at
269    /// the serialization boundary. Identity, `result`, `warnings`,
270    /// `next_actions`, and `runtime_error` are untouched, so no correctness or
271    /// truncation signal is lost.
272    pub fn drop_telemetry(&mut self) {
273        self.telemetry = None;
274    }
275
276    /// Drain project-lifetime advisories into `warnings`. Called once by
277    /// [`crate::server`] just before serialization, for both `ok` and
278    /// `runtime_unavailable` responses.
279    pub(crate) fn drain_advisories(&mut self) {
280        let advisories = std::mem::take(&mut self.advisories);
281        self.warnings.extend(advisories);
282    }
283
284    #[must_use]
285    pub fn warn(mut self, msg: impl Into<String>) -> Self {
286        self.warnings.push(msg.into());
287        self
288    }
289
290    #[must_use]
291    pub fn hint(mut self, msg: impl Into<String>) -> Self {
292        self.next_actions.push(msg.into());
293        self
294    }
295}
296
297#[cfg(test)]
298#[allow(clippy::unwrap_used)]
299mod tests {
300    use super::*;
301
302    #[test]
303    fn runtime_facts_separate_call_restart_from_lifecycle_history() {
304        let facts = RuntimeFacts {
305            worker_generation: 4,
306            worker_restarted: false,
307            retry_count: 0,
308            admission_wait_millis: 0,
309            queue_wait_millis: 0,
310            call_restart: None,
311            last_restart: Some(RuntimeRestartEvent {
312                cause: "rss_post_job".to_owned(),
313                reason: "rss_post_job current_kib=5 limit_kib=4".to_owned(),
314                worker_generation: 3,
315                planned: true,
316                rss_kib: Some(5),
317                limit_kib: Some(4),
318            }),
319            rss_kib: Some(2),
320            worker_lanes: 1,
321            import_profile: Some("Init".to_owned()),
322            profile_switch_count: 1,
323            restarts_total: 1,
324            restarts_by_cause: BTreeMap::from([("rss_post_job".to_owned(), 1)]),
325        };
326
327        let json = serde_json::to_value(facts).unwrap();
328        assert!(json.pointer("/call_restart").is_none_or(serde_json::Value::is_null));
329        assert_eq!(
330            json.pointer("/last_restart/cause").and_then(serde_json::Value::as_str),
331            Some("rss_post_job")
332        );
333        assert_eq!(
334            json.pointer("/worker_restarted").and_then(serde_json::Value::as_bool),
335            Some(false)
336        );
337    }
338}
lean_host_mcp/envelope.rs

lean_host_mcp/
envelope.rs
