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    /// The ACP agent `run_started` records for a harness run
55    /// (`crates/kernel/spec/Event/Record.lean` §8-87); `None` for a run this
56    /// city's own model loop drives.
57    pub agent: Option<&'a kernel::event::record::AgentRunIdentity>,
58}
59
60impl RunPlan {
61    /// The charter a model run opens and closes with, lent from its own
62    /// constants.
63    pub fn charter(&self) -> Charter<'_> {
64        Charter {
65            run: self.run,
66            who: &self.who,
67            addr: &self.addr,
68            task: &self.task,
69            goal: &self.goal,
70            job: &self.job,
71            parent: self.parent,
72            predecessor: self.predecessor,
73            dispatched_by: &self.dispatched_by,
74            skills: &self.skills,
75            policy: self.run_policy.reader().now(),
76            naming: self.naming,
77            opening: Some(self.opening),
78            effort: self.shape.effort,
79            agent: None,
80        }
81    }
82}
83
84impl Charter<'_> {
85    /// The dispatch pair: the job pin lands first, then the run exists.
86    /// Two lines, two clock samples - the pin is a fact about the city
87    /// and the start is a fact about the run.
88    ///
89    /// # Errors
90    /// Propagates the clock and the ledger.
91    pub(crate) fn open(
92        &self,
93        ledger: &mut dyn Ledger,
94        now: &mut dyn FnMut() -> Result<TimeMs, AxError>,
95    ) -> Result<(), AxError> {
96        let pin = CheckpointCommitted::JobPinned {
97            job: self.job.clone(),
98        };
99        ledger.append(EventDraft {
100            run: RunId::CITY,
101            t: now()?,
102            who: Who::City.to_string(),
103            addr: Some(self.addr.clone()),
104            kind: EventKind::CheckpointCommitted,
105            data: Payload::of(&pin)?,
106            ig: false,
107        })?;
108        let started = RunStarted {
109            task: self.task.to_owned(),
110            goal: self.goal.to_owned(),
111            job: Some(self.job.clone()),
112            parent: self.parent,
113            predecessor: self.predecessor,
114            skills: self.skills.to_vec(),
115            dispatched_by: Some(self.dispatched_by.clone()),
116            policy: Some(self.policy),
117            naming: self.naming,
118            opening: self.opening,
119            effort: self.effort,
120            agent: self.agent.cloned(),
121        };
122        ledger.append(EventDraft {
123            run: self.run,
124            t: now()?,
125            who: Who::City.to_string(),
126            addr: Some(self.addr.clone()),
127            kind: EventKind::RunStarted,
128            data: Payload::of(&started)?,
129            ig: false,
130        })?;
131        Ok(())
132    }
133
134    /// The closing pair: the handoff at `t`, and `run_frozen` one
135    /// millisecond later, because the two lines record one event.
136    ///
137    /// # Errors
138    /// Propagates the ledger, and refuses a `t` at the end of `u64`.
139    pub(crate) fn close(
140        &self,
141        ledger: &mut dyn Ledger,
142        handoff: &Handoff,
143        completion: &Completion,
144        t: TimeMs,
145    ) -> Result<(), AxError> {
146        ledger.append(EventDraft {
147            run: self.run,
148            t,
149            who: self.who.to_owned(),
150            addr: None,
151            kind: EventKind::HandoffWritten,
152            data: handoff.payload()?,
153            ig: false,
154        })?;
155        let closing = t.value().checked_add(1).ok_or_else(|| {
156            AxError::failure(AxCode::InvalidArgs, "stamp run_frozen", "u64 overflow")
157                .with_recovery("check the clock the caller injected")
158        })?;
159        ledger.append(EventDraft {
160            run: self.run,
161            t: TimeMs::new(closing),
162            who: self.who.to_owned(),
163            addr: None,
164            kind: EventKind::RunFrozen,
165            data: Payload::of(&RunFrozen::of(completion))?,
166            ig: false,
167        })?;
168        Ok(())
169    }
170
171    /// One line of this run, written as its resident at its address.
172    pub(crate) fn line(&self, kind: EventKind, data: Payload, t: TimeMs) -> EventDraft {
173        EventDraft {
174            run: self.run,
175            t,
176            who: self.who.to_owned(),
177            addr: Some(self.addr.clone()),
178            kind,
179            data,
180            ig: false,
181        }
182    }
183}
runtime/run/charter.rs

runtime/run/
charter.rs
