logicaffeine_kernel/interface/lean/
diagnostic.rs

1//! Typed, machine-readable reasons for every refusal the Lean reader gives.
2//!
3//! A [`Verdict`](super::Verdict) says *whether* the kernel refused (`Reject`: the input is wrong;
4//! `Decline`: the input may be right but is not accepted). A [`Reason`] says *why*, as a stable
5//! [`DiagnosticCode`] a program can dispatch on, plus the human message and, where known, the export
6//! line and the Lean declaration it arose in. The message is still what the reader always printed,
7//! so the benchmark protocol's text output is unchanged.
8//!
9//! Every code belongs to exactly one [`Outcome`] of the `logos-lean-result/1` contract, and every
10//! outcome has one exit code, so a consumer can dispatch on the outcome and drill into the code.
11
12use std::fmt;
13
14/// Why the reader (or the intake around it) refused. Stable across releases: the wire name is
15/// [`DiagnosticCode::as_str`], and a renamed wire name is a protocol break.
16#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)]
17pub enum DiagnosticCode {
18    /// Well-formed input whose mathematics the kernel refutes: an ill-typed body, a type mismatch,
19    /// a positivity violation.
20    InvalidProof,
21    /// The export itself is malformed: bad JSON, a dangling index, a missing mandatory field.
22    MalformedExport,
23    /// The export declares a format version this reader does not implement.
24    UnsupportedExportVersion,
25    /// The export or project was produced by a Lean or exporter outside the pinned profile.
26    UnsupportedToolchain,
27    /// A record, expression or declaration kind the pinned export format does not define.
28    UnknownRecordKind,
29    /// A field the pinned export format does not define for its record.
30    UnknownField,
31    /// A metavariable or free variable: the declaration was never fully elaborated.
32    UnresolvedMetavariable,
33    /// A declaration the input names but never declares, or a target that is not there.
34    MissingDeclaration,
35    /// A declaration declared twice.
36    DuplicateDeclaration,
37    /// A Lean project imports a module that is neither in the project nor in Lean core.
38    MissingModule,
39    /// A Lean project's modules import each other in a cycle.
40    ImportCycle,
41    /// Lean itself rejected the project's source (syntax or elaboration), at Lean's location.
42    LeanRejected,
43    /// The input is a pre-exported artifact: this run did not observe Lean accepting its source.
44    LeanAcceptanceNotObserved,
45    /// Valid Lean that LOGOS does not yet express faithfully; declined, never approximated.
46    UnsupportedFeature,
47    /// The independent re-checker did not confirm what the primary kernel accepted.
48    RecheckRefused,
49    /// The transitive assumption audit could not be completed.
50    AuditIncomplete,
51    /// The declaration depends on an assumption the policy does not allow.
52    DisallowedAssumption,
53    /// Lean's `#print axioms` and the LOGOS audit disagree on a declaration's assumptions.
54    AssumptionDisagreement,
55    /// A declared resource budget was exhausted before a decision.
56    ResourceLimit,
57    /// The environment failed: a file could not be read, a tool is absent, a thread could not be
58    /// reserved.
59    Infrastructure,
60    /// LOGOS's own artifact — the emitted document, the assembled package, its fresh replay —
61    /// failed its self-verification after every check of the user's input passed. The fault is
62    /// ours, never the user's mathematics.
63    InternalInconsistency,
64    /// The command was invoked wrongly; nothing ran.
65    Usage,
66    /// Not yet classified. `lean_diagnostic_code_lock` drives the number of such sites to zero.
67    Unclassified,
68}
69
70impl DiagnosticCode {
71    pub const ALL: [DiagnosticCode; 23] = [
72        DiagnosticCode::InvalidProof,
73        DiagnosticCode::MalformedExport,
74        DiagnosticCode::UnsupportedExportVersion,
75        DiagnosticCode::UnsupportedToolchain,
76        DiagnosticCode::UnknownRecordKind,
77        DiagnosticCode::UnknownField,
78        DiagnosticCode::UnresolvedMetavariable,
79        DiagnosticCode::MissingDeclaration,
80        DiagnosticCode::DuplicateDeclaration,
81        DiagnosticCode::MissingModule,
82        DiagnosticCode::ImportCycle,
83        DiagnosticCode::LeanRejected,
84        DiagnosticCode::LeanAcceptanceNotObserved,
85        DiagnosticCode::UnsupportedFeature,
86        DiagnosticCode::RecheckRefused,
87        DiagnosticCode::AuditIncomplete,
88        DiagnosticCode::DisallowedAssumption,
89        DiagnosticCode::AssumptionDisagreement,
90        DiagnosticCode::ResourceLimit,
91        DiagnosticCode::Infrastructure,
92        DiagnosticCode::InternalInconsistency,
93        DiagnosticCode::Usage,
94        DiagnosticCode::Unclassified,
95    ];
96
97    pub fn as_str(self) -> &'static str {
98        match self {
99            DiagnosticCode::InvalidProof => "invalid_proof",
100            DiagnosticCode::MalformedExport => "malformed_export",
101            DiagnosticCode::UnsupportedExportVersion => "unsupported_export_version",
102            DiagnosticCode::UnsupportedToolchain => "unsupported_toolchain",
103            DiagnosticCode::UnknownRecordKind => "unknown_record_kind",
104            DiagnosticCode::UnknownField => "unknown_field",
105            DiagnosticCode::UnresolvedMetavariable => "unresolved_metavariable",
106            DiagnosticCode::MissingDeclaration => "missing_declaration",
107            DiagnosticCode::DuplicateDeclaration => "duplicate_declaration",
108            DiagnosticCode::MissingModule => "missing_module",
109            DiagnosticCode::ImportCycle => "import_cycle",
110            DiagnosticCode::LeanRejected => "lean_rejected",
111            DiagnosticCode::LeanAcceptanceNotObserved => "lean_acceptance_not_observed",
112            DiagnosticCode::UnsupportedFeature => "unsupported_feature",
113            DiagnosticCode::RecheckRefused => "recheck_refused",
114            DiagnosticCode::AuditIncomplete => "audit_incomplete",
115            DiagnosticCode::DisallowedAssumption => "disallowed_assumption",
116            DiagnosticCode::AssumptionDisagreement => "assumption_disagreement",
117            DiagnosticCode::ResourceLimit => "resource_limit",
118            DiagnosticCode::Infrastructure => "infrastructure",
119            DiagnosticCode::InternalInconsistency => "internal_inconsistency",
120            DiagnosticCode::Usage => "usage",
121            DiagnosticCode::Unclassified => "unclassified",
122        }
123    }
124
125    /// The code a wire name names.
126    pub fn from_wire(wire: &str) -> Option<Self> {
127        Self::ALL.into_iter().find(|code| code.as_str() == wire)
128    }
129
130    /// The result outcome this code decides. `Usage` precedes any result; `Unclassified` carries no
131    /// category of its own (see [`Outcome::of_refusal`]).
132    pub fn outcome(self) -> Option<Outcome> {
133        use DiagnosticCode as C;
134        Some(match self {
135            C::InvalidProof
136            | C::MalformedExport
137            | C::UnresolvedMetavariable
138            | C::MissingDeclaration
139            | C::DuplicateDeclaration
140            | C::MissingModule
141            | C::ImportCycle
142            | C::LeanRejected => Outcome::InvalidSource,
143            C::UnsupportedExportVersion
144            | C::UnsupportedToolchain
145            | C::UnknownRecordKind
146            | C::UnknownField
147            | C::LeanAcceptanceNotObserved
148            | C::UnsupportedFeature
149            | C::RecheckRefused
150            | C::AuditIncomplete => Outcome::UnsupportedFeature,
151            C::DisallowedAssumption | C::AssumptionDisagreement => Outcome::DisallowedAssumptions,
152            C::ResourceLimit => Outcome::ResourceLimit,
153            C::Infrastructure | C::InternalInconsistency => Outcome::InfrastructureFailure,
154            C::Usage | C::Unclassified => return None,
155        })
156    }
157}
158
159impl fmt::Display for DiagnosticCode {
160    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
161        f.write_str(self.as_str())
162    }
163}
164
165/// The outcome of a `logos-lean-result/1` document, with the contract's exit code.
166#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)]
167pub enum Outcome {
168    /// Every stage passed.
169    Verified,
170    /// A real rejection: the source, the export or the proof is wrong.
171    InvalidSource,
172    /// Valid input LOGOS does not (yet) carry to a verified result.
173    UnsupportedFeature,
174    /// The result depends on an assumption outside the policy.
175    DisallowedAssumptions,
176    /// A declared budget ran out before a decision.
177    ResourceLimit,
178    /// The environment failed; nothing was decided about the input.
179    InfrastructureFailure,
180}
181
182impl Outcome {
183    pub const ALL: [Outcome; 6] = [
184        Outcome::Verified,
185        Outcome::InvalidSource,
186        Outcome::UnsupportedFeature,
187        Outcome::DisallowedAssumptions,
188        Outcome::ResourceLimit,
189        Outcome::InfrastructureFailure,
190    ];
191
192    pub fn as_str(self) -> &'static str {
193        match self {
194            Outcome::Verified => "verified",
195            Outcome::InvalidSource => "invalid_source",
196            Outcome::UnsupportedFeature => "unsupported_feature",
197            Outcome::DisallowedAssumptions => "disallowed_assumptions",
198            Outcome::ResourceLimit => "resource_limit",
199            Outcome::InfrastructureFailure => "infrastructure_failure",
200        }
201    }
202
203    /// The contract's exit code: 0 verified · 1 invalid source · 2 unsupported feature ·
204    /// 3 disallowed assumptions · 4 resource limit · 5 infrastructure failure.
205    pub fn exit_code(self) -> i32 {
206        match self {
207            Outcome::Verified => 0,
208            Outcome::InvalidSource => 1,
209            Outcome::UnsupportedFeature => 2,
210            Outcome::DisallowedAssumptions => 3,
211            Outcome::ResourceLimit => 4,
212            Outcome::InfrastructureFailure => 5,
213        }
214    }
215
216    /// The outcome of a refusal: its code's outcome, or — for a code without one — the verdict
217    /// kind's benchmark meaning (a rejection is invalid source, a decline an unsupported feature).
218    pub fn of_refusal(code: DiagnosticCode, rejected: bool) -> Outcome {
219        code.outcome().unwrap_or(if rejected {
220            Outcome::InvalidSource
221        } else {
222            Outcome::UnsupportedFeature
223        })
224    }
225}
226
227impl fmt::Display for Outcome {
228    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
229        f.write_str(self.as_str())
230    }
231}
232
233/// A refusal's code and message, and where it arose when that is known. Dereferences to the
234/// message, so a reason reads as the text the reader has always reported.
235#[derive(Clone, PartialEq, Eq)]
236pub struct Reason {
237    code: DiagnosticCode,
238    message: String,
239    line: Option<usize>,
240    declaration: Option<String>,
241    stage: Option<&'static str>,
242}
243
244impl Reason {
245    pub fn new(code: DiagnosticCode, message: impl Into<String>) -> Self {
246        Reason {
247            code,
248            message: message.into(),
249            line: None,
250            declaration: None,
251            stage: None,
252        }
253    }
254    pub fn code(&self) -> DiagnosticCode {
255        self.code
256    }
257    /// The receipt stage the refusal arose at, when the code alone does not say: a resource limit
258    /// reached by the independent kernel belongs to `independent_recheck`, not to translation.
259    pub fn stage(&self) -> Option<&'static str> {
260        self.stage
261    }
262    /// The same reason, recorded as arising at receipt stage `stage`.
263    pub fn at_stage(self, stage: &'static str) -> Self {
264        Reason {
265            stage: Some(stage),
266            ..self
267        }
268    }
269    pub fn message(&self) -> &str {
270        &self.message
271    }
272    /// The 1-based line of the input the refusal arose at.
273    pub fn line(&self) -> Option<usize> {
274        self.line
275    }
276    /// The Lean declaration (dotted name) the refusal arose in.
277    pub fn declaration(&self) -> Option<&str> {
278        self.declaration.as_deref()
279    }
280    /// The same reason, its message prefixed with where it arose.
281    pub fn located(self, prefix: impl fmt::Display) -> Self {
282        Reason {
283            message: format!("{prefix}: {}", self.message),
284            ..self
285        }
286    }
287    /// The same reason and message, recorded as arising at `line`. The innermost line wins: a
288    /// reason already located keeps its line.
289    pub fn at_line(self, line: usize) -> Self {
290        Reason {
291            line: self.line.or(Some(line)),
292            ..self
293        }
294    }
295    /// The same reason and message, recorded as arising in `declaration`. The innermost wins.
296    pub fn in_declaration(self, declaration: impl Into<String>) -> Self {
297        let declaration = self
298            .declaration
299            .clone()
300            .or_else(|| Some(declaration.into()));
301        Reason {
302            declaration,
303            ..self
304        }
305    }
306}
307
308impl std::ops::Deref for Reason {
309    type Target = str;
310    fn deref(&self) -> &str {
311        &self.message
312    }
313}
314
315impl fmt::Display for Reason {
316    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
317        f.write_str(&self.message)
318    }
319}
320
321/// Prints as the message string did, so `{verdict:?}` output is unchanged for protocol consumers.
322impl fmt::Debug for Reason {
323    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
324        fmt::Debug::fmt(&self.message, f)
325    }
326}
logicaffeine_kernel/interface/lean/diagnostic.rs

logicaffeine_kernel/interface/lean/
diagnostic.rs
