runtime/run/
charter.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//! A run's opening pair and its closing pair, written once for every
7//! kind of run (`crates/runtime/spec/Run.lean` §8-52, runtime D7).
8//!
9//! A model run and a harness run open and close alike: the job pin, then
10//! `run_started`; `handoff_written`, then `run_frozen` a millisecond
11//! later. What differs is what happens between, and only a model run has
12//! a `RunPlan` to say it, so the pairs are written from a view both kinds
13//! of run can lend.
14
15use kernel::event::Who;
16use kernel::event::record::{CheckpointCommitted, Opening, RunFrozen, RunStarted};
17use kernel::{
18    Address, AxCode, AxError, Completion, EventDraft, EventKind, Ledger, Locator, Payload, RunId,
19    TimeMs,
20};
21
22use crate::catalog::SkillPin;
23use crate::handoff::Handoff;
24
25use super::RunPlan;
26
27/// What `run_started` records about a run, and whom every line of the
28/// run is written as.
29#[derive(Debug, Clone, Copy)]
30pub struct Charter<'a> {
31    pub run: RunId,
32    /// The resident the run's lines are written as.
33    pub who: &'a str,
34    pub addr: &'a Address,
35    pub task: &'a str,
36    pub goal: &'a str,
37    pub job: &'a Locator,
38    pub parent: Option<RunId>,
39    pub predecessor: Option<RunId>,
40    pub dispatched_by: &'a Who,
41    pub skills: &'a [SkillPin],
42    /// The run policy `run_started` records (`crates/kernel/Spec.lean` §8-77).
43    pub policy: kernel::RunPolicy,
44    /// The identity version `run_started` records (`crates/kernel/Spec.lean` §8-79).
45    pub naming: Option<kernel::B3Hash>,
46    /// How the run's first user message was written, which a fork reads
47    /// back (`crates/kernel/Spec.lean` §8-82-1); `None` for a run the city writes no
48    /// first message for.
49    pub opening: Option<Opening>,
50    /// The effort `run_started` records (`crates/kernel/Spec.lean` §8-85):
51    /// the one the run's requests froze; `None` when none was stated, and
52    /// for a run that sends this city no requests.
53    pub effort: Option<kernel::Effort>,
54}
55
56impl RunPlan {
57    /// The charter a model run opens and closes with, lent from its own
58    /// constants.
59    pub fn charter(&self) -> Charter<'_> {
60        Charter {
61            run: self.run,
62            who: &self.who,
63            addr: &self.addr,
64            task: &self.task,
65            goal: &self.goal,
66            job: &self.job,
67            parent: self.parent,
68            predecessor: self.predecessor,
69            dispatched_by: &self.dispatched_by,
70            skills: &self.skills,
71            policy: self.run_policy,
72            naming: self.naming,
73            opening: Some(self.opening),
74            effort: self.shape.effort,
75        }
76    }
77}
78
79impl Charter<'_> {
80    /// The dispatch pair: the job pin lands first, then the run exists.
81    /// Two lines, two clock samples - the pin is a fact about the city
82    /// and the start is a fact about the run.
83    ///
84    /// # Errors
85    /// Propagates the clock and the ledger.
86    pub(crate) fn open(
87        &self,
88        ledger: &mut dyn Ledger,
89        now: &mut dyn FnMut() -> Result<TimeMs, AxError>,
90    ) -> Result<(), AxError> {
91        let pin = CheckpointCommitted::JobPinned {
92            job: self.job.clone(),
93        };
94        ledger.append(EventDraft {
95            run: RunId::CITY,
96            t: now()?,
97            who: Who::City.to_string(),
98            addr: Some(self.addr.clone()),
99            kind: EventKind::CheckpointCommitted,
100            data: Payload::of(&pin)?,
101            ig: false,
102        })?;
103        let started = RunStarted {
104            task: self.task.to_owned(),
105            goal: self.goal.to_owned(),
106            job: Some(self.job.clone()),
107            parent: self.parent,
108            predecessor: self.predecessor,
109            skills: self.skills.to_vec(),
110            dispatched_by: Some(self.dispatched_by.clone()),
111            policy: Some(self.policy),
112            naming: self.naming,
113            opening: self.opening,
114            effort: self.effort,
115        };
116        ledger.append(EventDraft {
117            run: self.run,
118            t: now()?,
119            who: Who::City.to_string(),
120            addr: Some(self.addr.clone()),
121            kind: EventKind::RunStarted,
122            data: Payload::of(&started)?,
123            ig: false,
124        })?;
125        Ok(())
126    }
127
128    /// The closing pair: the handoff at `t`, and `run_frozen` one
129    /// millisecond later, because the two lines record one event.
130    ///
131    /// # Errors
132    /// Propagates the ledger, and refuses a `t` at the end of `u64`.
133    pub(crate) fn close(
134        &self,
135        ledger: &mut dyn Ledger,
136        handoff: &Handoff,
137        completion: &Completion,
138        t: TimeMs,
139    ) -> Result<(), AxError> {
140        ledger.append(EventDraft {
141            run: self.run,
142            t,
143            who: self.who.to_owned(),
144            addr: None,
145            kind: EventKind::HandoffWritten,
146            data: handoff.payload()?,
147            ig: false,
148        })?;
149        let closing = t.value().checked_add(1).ok_or_else(|| {
150            AxError::failure(AxCode::InvalidArgs, "stamp run_frozen", "u64 overflow")
151                .with_recovery("check the clock the caller injected")
152        })?;
153        ledger.append(EventDraft {
154            run: self.run,
155            t: TimeMs::new(closing),
156            who: self.who.to_owned(),
157            addr: None,
158            kind: EventKind::RunFrozen,
159            data: Payload::of(&RunFrozen::of(completion))?,
160            ig: false,
161        })?;
162        Ok(())
163    }
164
165    /// One line of this run, written as its resident at its address.
166    pub(crate) fn line(&self, kind: EventKind, data: Payload, t: TimeMs) -> EventDraft {
167        EventDraft {
168            run: self.run,
169            t,
170            who: self.who.to_owned(),
171            addr: Some(self.addr.clone()),
172            kind,
173            data,
174            ig: false,
175        }
176    }
177}
runtime/run/charter.rs

runtime/run/
charter.rs
