lean_host_mcp/
envelope.rs

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

lean_host_mcp/
envelope.rs
