logicaffeine_kernel/interface/lean/
receipt.rs

1//! The stages a Lean → LOGOS result passes through, named separately so that no result is ever one
2//! unexplained "verified" Boolean (competition rule R1). The names are the contract's wire names.
3
4/// Every stage, in the order a result passes through them.
5pub const STAGES: [&str; 7] = [
6    "lean_accepted",
7    "translated",
8    "primary_check",
9    "independent_recheck",
10    "assumption_policy",
11    "emission_reparsed",
12    "fresh_replay",
13];
14
15/// The stages a replay establishes from a package's bytes alone. `lean_accepted` is not among them:
16/// a replay never runs Lean, and says so rather than inheriting the producing run's word.
17pub const REPLAY_STAGES: [&str; 6] = [
18    "translated",
19    "primary_check",
20    "independent_recheck",
21    "assumption_policy",
22    "emission_reparsed",
23    "fresh_replay",
24];
25
26/// What happened in one stage. `NotRun` and `Unsupported` are never a pass.
27#[derive(Clone, Copy, Debug, PartialEq, Eq)]
28pub enum StageStatus {
29    Passed,
30    Failed,
31    NotRun,
32    Unsupported,
33}
34
35impl StageStatus {
36    pub fn as_str(self) -> &'static str {
37        match self {
38            StageStatus::Passed => "passed",
39            StageStatus::Failed => "failed",
40            StageStatus::NotRun => "not_run",
41            StageStatus::Unsupported => "unsupported",
42        }
43    }
44
45    /// The status a wire name denotes.
46    pub fn parse(name: &str) -> Option<StageStatus> {
47        match name {
48            "passed" => Some(StageStatus::Passed),
49            "failed" => Some(StageStatus::Failed),
50            "not_run" => Some(StageStatus::NotRun),
51            "unsupported" => Some(StageStatus::Unsupported),
52            _ => None,
53        }
54    }
55}
56
57#[derive(Clone, Debug, PartialEq, Eq)]
58pub struct Stage {
59    pub name: &'static str,
60    pub status: StageStatus,
61    pub detail: String,
62    /// The machine-readable reason a stage failed or was unsupported, when it did.
63    pub code: Option<String>,
64}
65
66/// A receipt: one entry per stage in [`STAGES`], in order. Verified only when every stage passed.
67#[derive(Clone, Debug, PartialEq, Eq)]
68pub struct Receipt {
69    pub stages: Vec<Stage>,
70}
71
72impl Receipt {
73    /// A receipt in which nothing has run yet.
74    pub fn unstarted() -> Self {
75        Receipt {
76            stages: STAGES
77                .iter()
78                .map(|name| Stage {
79                    name,
80                    status: StageStatus::NotRun,
81                    detail: String::new(),
82                    code: None,
83                })
84                .collect(),
85        }
86    }
87    pub fn stage(&self, name: &str) -> Option<&Stage> {
88        self.stages.iter().find(|s| s.name == name)
89    }
90    pub fn set(&mut self, name: &str, status: StageStatus, detail: impl Into<String>) {
91        let stage = self
92            .stages
93            .iter_mut()
94            .find(|s| s.name == name)
95            .unwrap_or_else(|| panic!("{name} is not a receipt stage"));
96        stage.status = status;
97        stage.detail = detail.into();
98        stage.code = None;
99    }
100    /// [`Receipt::set`] with the machine-readable reason.
101    pub fn set_with_code(
102        &mut self,
103        name: &str,
104        status: StageStatus,
105        code: &str,
106        detail: impl Into<String>,
107    ) {
108        self.set(name, status, detail);
109        self.stages
110            .iter_mut()
111            .find(|s| s.name == name)
112            .expect("set above")
113            .code = Some(code.to_string());
114    }
115    pub fn status(&self, name: &str) -> StageStatus {
116        self.stage(name).map_or(StageStatus::NotRun, |s| s.status)
117    }
118    pub fn verified(&self) -> bool {
119        self.stages.len() == STAGES.len()
120            && self.stages.iter().all(|s| s.status == StageStatus::Passed)
121    }
122    /// Every stage a replay establishes passed. Not the same as [`Receipt::verified`]: a replay
123    /// establishes everything except that the pinned Lean accepted the source, which only the
124    /// producing run observes.
125    pub fn replayed(&self) -> bool {
126        self.stages.len() == STAGES.len()
127            && REPLAY_STAGES
128                .iter()
129                .all(|name| self.status(name) == StageStatus::Passed)
130    }
131    /// The first stage that failed, in stage order.
132    pub fn first_failure(&self) -> Option<&Stage> {
133        self.stages.iter().find(|s| s.status == StageStatus::Failed)
134    }
135    /// The receipt as the contract's `stages` object, with a detail and code for each stage.
136    pub fn to_json(&self) -> serde_json::Value {
137        let mut stages = serde_json::Map::new();
138        for stage in &self.stages {
139            stages.insert(
140                stage.name.to_string(),
141                serde_json::json!({ "status": stage.status.as_str(), "code": stage.code, "detail": stage.detail }),
142            );
143        }
144        serde_json::Value::Object(stages)
145    }
146}
logicaffeine_kernel/interface/lean/receipt.rs

logicaffeine_kernel/interface/lean/
receipt.rs
