kernel/
completion.rs

1// This Source Code Form is subject to the terms of the Mozilla Public
2// License, v. 2.0. If a copy of the MPL was not distributed with this
3// file, You can obtain one at https://mozilla.org/MPL/2.0/.
4// Copyright (c) 2026 2youg1 and the sprawling contributors
5
6//! Completion and progress. Claiming done makes
7//! nothing done: `Completion::Done` cannot be built without evidence the
8//! city recorded itself (the runtime checks depth). Progress
9//! is honest in the type: only a planned run owns a ratio method —
10//! an unplanned run has nothing to ask a percentage from.
11//! The part `crates/kernel/spec/Completion.lean` specifies this module.
12
13use serde::{Deserialize, Serialize};
14use serde_json::{Map, Value};
15
16use crate::budget::BudgetUse;
17use crate::error::{AxCode, AxError};
18use crate::event::{EventKind, EventRef};
19
20/// The kinds evidence may cite: the records the city wrote itself of an
21/// answer to a request it sent. [`Evidence::new`] and
22/// `registry::Artifact::verify` both read this one table, and a refusal
23/// names its kinds from here.
24pub(crate) const CITABLE: [EventKind; 3] = [
25    EventKind::ToolResult,
26    EventKind::ModelReturned,
27    EventKind::HarnessAnswered,
28];
29
30/// Non-empty, and every ref kind is in `CITABLE`.
31/// There is no other constructor and no Deserialize anywhere in the
32/// chain — history cannot be claimed, only cited.
33#[derive(Debug, Clone, PartialEq, Eq)]
34pub struct Evidence(Vec<EventRef>);
35
36impl Evidence {
37    pub fn new(refs: Vec<EventRef>) -> Result<Evidence, AxError> {
38        if refs.is_empty() {
39            return Err(AxError::failure(
40                AxCode::EvidenceMissing,
41                "construct evidence",
42                "empty ref list",
43            )
44            .with_recovery(format!("cite at least one {} event", citable_words()?)));
45        }
46        if let Some(bad) = refs.iter().find(|r| !CITABLE.contains(&r.kind())) {
47            return Err(AxError::failure(
48                AxCode::EvidenceMissing,
49                "construct evidence",
50                format!("ref kind {:?}", bad.kind()),
51            )
52            .with_recovery(format!("evidence kinds are {} only", citable_words()?)));
53        }
54        Ok(Evidence(refs))
55    }
56
57    pub fn refs(&self) -> &[EventRef] {
58        &self.0
59    }
60}
61
62/// The [`CITABLE`] kinds as the Ledger spells them, joined for the
63/// recovery of a refusal.
64pub(crate) fn citable_words() -> Result<String, AxError> {
65    let words = CITABLE
66        .iter()
67        .map(|kind| {
68            serde_json::to_value(kind)
69                .map(|word| word.to_string())
70                .map_err(|err| {
71                    AxError::failure(
72                        AxCode::InvalidArgs,
73                        "spell a citable event kind",
74                        format!("{kind:?}"),
75                    )
76                    .with_recovery(format!(
77                        "JSON refused this event kind ({err}); cite an event whose kind \
78                         `sprawling replay` prints"
79                    ))
80                })
81        })
82        .collect::<Result<Vec<String>, AxError>>()?;
83    Ok(words.join(", "))
84}
85
86/// The three endings; a fourth cannot be represented (frozen surface,
87/// 14.1). `Limit` is not a kind of done — record limit, not completion.
88#[derive(Debug, Clone, PartialEq, Eq)]
89pub enum Completion {
90    Done(Evidence),
91    Limit,
92    Cancelled,
93}
94
95impl Completion {
96    pub fn name(&self) -> &'static str {
97        match self {
98            Completion::Done(_) => "done",
99            Completion::Limit => "limit",
100            Completion::Cancelled => "cancelled",
101        }
102    }
103
104    /// One-way projection into an event payload: `completion` plus, for
105    /// Done, the evidence as `{seq, kind}` pairs. Deliberately no serde —
106    /// deserializing a Completion would mint EventRefs out of thin air.
107    pub fn extend_payload(&self, map: &mut Map<String, Value>) -> Result<(), AxError> {
108        map.insert(
109            "completion".to_owned(),
110            Value::String(self.name().to_owned()),
111        );
112        if let Completion::Done(evidence) = self {
113            let mut cited = Vec::new();
114            for r in evidence.refs() {
115                let mut entry = Map::new();
116                entry.insert("seq".to_owned(), Value::Number(r.seq().value().into()));
117                entry.insert(
118                    "kind".to_owned(),
119                    serde_json::to_value(r.kind()).map_err(|err| {
120                        AxError::failure(
121                            AxCode::InvalidArgs,
122                            "encode evidence",
123                            format!("event kind at seq {}", r.seq().value()),
124                        )
125                        .with_recovery(format!(
126                            "JSON refused this event kind ({err}); cite an event whose kind \
127                             `sprawling replay --seq {}` prints",
128                            r.seq().value()
129                        ))
130                    })?,
131                );
132                cited.push(Value::Object(entry));
133            }
134            map.insert("evidence".to_owned(), Value::Array(cited));
135        }
136        Ok(())
137    }
138}
139
140/// Progress with a denominator: the leaves of the plan tree.
141///
142/// Unlike [`Completion`], progress carries serde: it is a reading of a
143/// file that the interface renders, not a claim that work finished. What
144/// must not be deserialisable is a `Done` — and that still is not.
145///
146/// **Two figures, because either alone misleads.** The share says how
147/// much of the plan is behind you and moves when a branch is divided
148/// generously; the leaf count says how many pieces the plan turned out
149/// to have and does not. A reader seeing `83% / 4 leaves left` can tell
150/// the difference between work finished and work redistributed, and a
151/// reader seeing one number cannot.
152#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
153#[cfg_attr(feature = "schema", derive(schemars::JsonSchema))]
154pub struct PlannedProgress {
155    pub done: u32,
156    pub blocked: u32,
157    pub total: u32,
158    /// The share of the whole plan that is done, in billionths
159    /// (`kernel::share::WHOLE_PPB`). An integer, so two readings compare
160    /// the same way on every machine.
161    pub done_ppb: u64,
162    /// The share that is blocked or waiting for a person.
163    pub blocked_ppb: u64,
164}
165
166impl PlannedProgress {
167    /// `(done, total)` — the renderer computes its own percentage from a
168    /// real fraction, never from a claim.
169    pub fn ratio(&self) -> (u32, u32) {
170        (self.done, self.total)
171    }
172
173    /// `(done, whole)` in billionths: the same reading weighted by how
174    /// the plan divides itself, rather than by how many rows it has.
175    pub fn weighted(&self) -> (u64, u64) {
176        (self.done_ppb, crate::share::WHOLE_PPB)
177    }
178}
179
180/// Progress without a denominator: steps walked and budget burned. No
181/// ratio method exists — the interface cannot paint what it cannot know
182/// (A17's type half).
183#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
184#[cfg_attr(feature = "schema", derive(schemars::JsonSchema))]
185pub struct UnplannedProgress {
186    pub steps: u32,
187    pub budget: BudgetUse,
188}
189
190/// Deliberately exhaustive: both faces must be handled by every renderer.
191#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
192#[serde(rename_all = "snake_case")]
193#[cfg_attr(feature = "schema", derive(schemars::JsonSchema))]
194pub enum Progress {
195    Planned(PlannedProgress),
196    Unplanned(UnplannedProgress),
197}
198
199#[cfg(test)]
200#[allow(
201    clippy::unwrap_used,
202    clippy::expect_used,
203    clippy::panic,
204    clippy::indexing_slicing,
205    reason = "test code"
206)]
207mod tests {
208    use super::*;
209    use crate::event::{EventDraft, EventRecord, Payload, RunId, Seq, TimeMs};
210    use crate::ledger::GENESIS_PREV;
211
212    fn evidence_ref(kind: EventKind) -> EventRef {
213        let draft = EventDraft {
214            run: RunId::CITY,
215            t: TimeMs::new(0),
216            who: "city".into(),
217            addr: None,
218            kind,
219            data: Payload::empty(),
220            ig: false,
221        };
222        EventRecord::from_draft(draft, Seq::FIRST, GENESIS_PREV).to_ref()
223    }
224
225    #[test]
226    fn empty_or_wrong_kind_evidence_cannot_be_built() {
227        assert_eq!(
228            Evidence::new(vec![]).unwrap_err().code(),
229            &AxCode::EvidenceMissing
230        );
231        let err = Evidence::new(vec![evidence_ref(EventKind::RunStarted)]).unwrap_err();
232        assert_eq!(err.code(), &AxCode::EvidenceMissing);
233    }
234
235    #[test]
236    fn a_harness_answer_is_evidence() {
237        assert!(Evidence::new(vec![evidence_ref(EventKind::HarnessAnswered)]).is_ok());
238        let err = Evidence::new(vec![evidence_ref(EventKind::HarnessReported)]).unwrap_err();
239        assert_eq!(err.code(), &AxCode::EvidenceMissing);
240        let recovery = err.recovery();
241        let at = |word: &str| recovery.find(word).unwrap();
242        assert!(at("tool_result") < at("model_returned"));
243        assert!(at("model_returned") < at("harness_answered"));
244    }
245
246    #[test]
247    fn done_payload_cites_its_evidence() {
248        let done =
249            Completion::Done(Evidence::new(vec![evidence_ref(EventKind::ModelReturned)]).unwrap());
250        let mut map = Map::new();
251        done.extend_payload(&mut map).unwrap();
252        assert_eq!(map["completion"], "done");
253        assert_eq!(map["evidence"][0]["kind"], "model_returned");
254        let mut map = Map::new();
255        Completion::Limit.extend_payload(&mut map).unwrap();
256        assert_eq!(map["completion"], "limit");
257        assert!(!map.contains_key("evidence"));
258    }
259
260    #[test]
261    fn only_planned_progress_owns_a_ratio() {
262        let planned = PlannedProgress {
263            done: 3,
264            blocked: 1,
265            total: 9,
266            done_ppb: 250_000_000,
267            blocked_ppb: 0,
268        };
269        assert_eq!(planned.ratio(), (3, 9));
270        assert_eq!(
271            planned.weighted(),
272            (250_000_000, crate::share::WHOLE_PPB),
273            "a quarter of the plan behind three of nine rows: the two \
274             figures are not the same reading"
275        );
276        // UnplannedProgress has no ratio method — nothing to assert at
277        // runtime; the trybuild case pins the absence.
278        let unplanned = UnplannedProgress {
279            steps: 12,
280            budget: BudgetUse::default(),
281        };
282        assert_eq!(unplanned.steps, 12);
283    }
284}
kernel/completion.rs

kernel/
completion.rs
