logicaffeine_kernel/dag/
error.rs

1//! Typed kernel verdicts.
2//!
3//! A `Reject` is a claim: the input is not a valid Lean environment. A `Decline` claims nothing:
4//! the checker ran out of a resource or met a construct it does not implement. The two are never
5//! confused, because a decline reported as a rejection would be a wrong answer on a valid proof.
6
7use std::fmt;
8
9#[derive(Clone, Copy, Debug, PartialEq, Eq)]
10pub enum FailKind {
11    /// The input is ill-formed or ill-typed.
12    Reject,
13    /// Resource exhaustion or an unsupported construct; no claim about validity.
14    Decline,
15    /// A speculative computation ran out of the budget its caller gave it. It never escapes the
16    /// caller that set the budget, which falls back to the complete path; should it escape, it
17    /// reads as a decline.
18    Exhausted,
19}
20
21#[derive(Clone, Debug)]
22pub struct Failure {
23    pub kind: FailKind,
24    pub message: String,
25    pub detail: Option<String>,
26    pub declaration: Option<String>,
27}
28
29/// A [`Failure`] behind one pointer. Every step of checking returns a [`KResult`], almost always
30/// `Ok`; boxed, the failure keeps `KResult<T>` as small as `T` plus a pointer, so results travel
31/// in registers instead of through memory on every call.
32#[derive(Clone)]
33pub struct KernelFailure(Box<Failure>);
34
35pub type KResult<T> = Result<T, KernelFailure>;
36
37const _: () = assert!(
38    std::mem::size_of::<KResult<()>>() == std::mem::size_of::<usize>(),
39    "a unit result is one pointer"
40);
41const _: () = assert!(
42    std::mem::size_of::<KResult<u32>>() <= 2 * std::mem::size_of::<usize>(),
43    "an id result fits in two registers"
44);
45
46impl std::ops::Deref for KernelFailure {
47    type Target = Failure;
48
49    fn deref(&self) -> &Failure {
50        &self.0
51    }
52}
53
54impl std::ops::DerefMut for KernelFailure {
55    fn deref_mut(&mut self) -> &mut Failure {
56        &mut self.0
57    }
58}
59
60impl fmt::Debug for KernelFailure {
61    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
62        self.0.fmt(f)
63    }
64}
65
66impl KernelFailure {
67    #[cold]
68    pub fn reject(message: impl Into<String>) -> KernelFailure {
69        KernelFailure(Box::new(Failure {
70            kind: FailKind::Reject,
71            message: message.into(),
72            detail: None,
73            declaration: None,
74        }))
75    }
76
77    #[cold]
78    pub fn resource(message: impl Into<String>) -> KernelFailure {
79        KernelFailure(Box::new(Failure {
80            kind: FailKind::Decline,
81            message: message.into(),
82            detail: None,
83            declaration: None,
84        }))
85    }
86
87    pub fn with_detail(mut self, detail: impl Into<String>) -> KernelFailure {
88        self.detail = Some(detail.into());
89        self
90    }
91
92    pub fn in_declaration(mut self, name: impl Into<String>) -> KernelFailure {
93        if self.declaration.is_none() {
94            self.declaration = Some(name.into());
95        }
96        self
97    }
98
99    #[cold]
100    pub fn exhausted() -> KernelFailure {
101        KernelFailure(Box::new(Failure {
102            kind: FailKind::Exhausted,
103            message: "speculation budget exhausted".into(),
104            detail: None,
105            declaration: None,
106        }))
107    }
108
109    pub fn is_exhausted(&self) -> bool {
110        self.kind == FailKind::Exhausted
111    }
112
113    pub fn is_reject(&self) -> bool {
114        self.kind == FailKind::Reject
115    }
116}
117
118impl fmt::Display for KernelFailure {
119    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
120        let verdict = match self.kind {
121            FailKind::Reject => "rejected",
122            FailKind::Decline | FailKind::Exhausted => "declined",
123        };
124        match &self.declaration {
125            Some(d) => write!(f, "{verdict}: declaration '{d}': {}", self.message)?,
126            None => write!(f, "{verdict}: {}", self.message)?,
127        }
128        if let Some(detail) = &self.detail {
129            write!(f, "\n  {detail}")?;
130        }
131        Ok(())
132    }
133}
logicaffeine_kernel/dag/error.rs

logicaffeine_kernel/dag/
error.rs
