Skip to main content

runtime/
mode.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//! Run modes and admission. A run sits in exactly one mode; the
7//! catalog lists only that one (progressive disclosure — the other
8//! mode's text stays out of the window).
9//!
10//! One exception, and it is one line long: [`dev_entry`] tells a run
11//! that this city's own code is changeable, and names the evidence a
12//! change can be asked to carry. Without it an agent working in this
13//! city never learns that the city's own code and SPECs are changeable
14//! at all, or under what discipline — and a capability nobody is told
15//! about is one nobody uses.
16//!
17//! The half that decides is [`admits`]: it says whether what a run
18//! produced may land, given the run policy it was dispatched under
19//! (`crates/runtime/spec/Mode.lean` §8-54). The evidence arrives as plain answers rather
20//! than as an instrument's type, because the instruments live in
21//! citysim, outside this crate, and the question here is not how
22//! evidence was gathered but whether enough of it exists.
23
24use crate::catalog::CatalogEntry;
25use kernel::{AdmissionRequirement, AxCode, AxError, LandingPolicy, Mode, RunPolicy};
26use std::sync::{Arc, PoisonError, RwLock};
27
28/// The name of the catalog row that opens the developer discipline.
29pub const DEV_ENTRY: &str = "dev";
30
31/// The row that tells a run this city is changeable, and nothing more.
32///
33/// One line in the resident segment, and the whole discipline behind an
34/// expansion. That split is the point: most sessions never change this
35/// city, so they pay a line; a session that is about to change it asks
36/// once and gets the evidence a change can be asked for, the reading
37/// order and what to do next. The same progressive disclosure the tool
38/// rows use, applied to the one capability an agent would otherwise
39/// never learn it has.
40#[must_use]
41pub fn dev_entry() -> CatalogEntry {
42    CatalogEntry {
43        name: DEV_ENTRY.to_owned(),
44        disclosure: "when the work is to change this city's own code, SPECs or tools, open this \
45                     entry before you touch anything"
46            .to_owned(),
47        expansion: "This city is built from small components, each with its SPEC beside it at \
48                    `crates/<crate>/<crate>-SPEC.md`. Read that SPEC, then the code, then the \
49                    tests next to the code - in that order, and before you change any of them. \
50                    Where the implementation would differ from the SPEC, the SPEC changes first \
51                    and says why.\n\nThe User chooses what a change must prove before it is \
52                    merged:\n- tested: the asset's own tests ran and passed.\n- contract_kept: \
53                    the asset's observable contract did not move.\n- double_validated: the change \
54                    holds on held-in and on held-out evidence.\nAnd where it lands: \
55                    ordinary work takes the building's own road, while an experiment works in a \
56                    tree of its own and nothing in it is merged.\n\nYour next step: say which \
57                    evidence this work needs and why, and wait for the User to dispatch it \
58                    with that requirement. Choosing a requirement does not provide the evidence."
59            .to_owned(),
60        // Text this build holds, not a document on a shelf: there is
61        // nothing behind it that could change while nobody is looking.
62        hash: None,
63        package: None,
64    }
65}
66
67/// The catalog row for this mode: disclosure one-liner plus the
68/// expansion text. The chat row is the whole of what chat mode does:
69/// one line telling the resident that the person is talking with it.
70#[must_use]
71pub fn catalog_entry(mode: Mode) -> CatalogEntry {
72    let (disclosure, expansion) = match mode {
73        Mode::Chat => (
74            "chat mode: focus on conversing with the User; answer what they said, in their language",
75            "Reply in the conversation. Start work, plans or dispatches only when the User asks for them.",
76        ),
77        Mode::Work => (
78            "work mode: carry out the task towards the stated goal; report when the goal is met",
79            "When the task asks for a plan first, write it into Roadmap.md with the `plan` tool \
80             before you change anything, then work through it. Report what you did and the \
81             evidence that the goal is met.",
82        ),
83    };
84    CatalogEntry {
85        name: format!("mode:{}", mode.as_str()),
86        disclosure: disclosure.to_owned(),
87        expansion: expansion.to_owned(),
88        hash: None,
89        package: None,
90    }
91}
92
93/// The resident tools a run in `mode` may run (`crates/runtime/Spec.lean`
94/// §8-60). The request carries the union of every mode's core
95/// ([`in_some_core`]), and [`mode_admits`] refuses at the call a tool the
96/// mode in force does not run; every other admitted tool waits in the
97/// dormant index. A name here travels only where the building admitted
98/// it: the hall registers no `exec`, so `exec` is in no tier there.
99///
100/// The two doors of the truncation lock are in every mode, because a
101/// dormant capability is reachable only through them. Chat answers the
102/// person and reads what it is asked about; work also edits and runs
103/// commands, which is what carrying out a task is made of. `status` is in
104/// both because the city prompt sends every resident to it for its
105/// situation.
106#[must_use]
107pub fn core_tools(mode: Mode) -> &'static [&'static str] {
108    match mode {
109        Mode::Chat => &[
110            crate::tools::CallTool::NAME,
111            crate::tools::DescribeTool::NAME,
112            crate::tools::ReadTool::NAME,
113            crate::tools::SearchTool::NAME,
114            crate::tools::StatusTool::NAME,
115        ],
116        Mode::Work => &[
117            crate::tools::CallTool::NAME,
118            crate::tools::DescribeTool::NAME,
119            crate::tools::EditTool::NAME,
120            kernel::ToolName::EXEC,
121            crate::tools::ReadTool::NAME,
122            crate::tools::SearchTool::NAME,
123            crate::tools::StatusTool::NAME,
124        ],
125    }
126}
127
128/// Whether `name` travels as a tool in every request of a session: it is
129/// in the core of some mode. The tool array is this union in every mode
130/// (runtime D25), so a change of mode mid-session leaves its bytes
131/// alone; [`mode_admits`] is where the mode in force still decides.
132#[must_use]
133pub fn in_some_core(name: &str) -> bool {
134    Mode::ALL
135        .iter()
136        .any(|mode| core_tools(*mode).contains(&name))
137}
138
139/// The gate a resident tool asks at its call: a tool that some mode
140/// carries and the mode in force does not is refused, before it does
141/// anything (runtime D25). A tool outside every core is the catalog's
142/// to reach through `call`, and this gate does not judge it.
143///
144/// # Errors
145/// `E_GATE_DENIED`, naming the tool and the mode, when the mode in
146/// force does not run it.
147pub fn mode_admits(policy: &RunPolicy, name: &str) -> Result<(), AxError> {
148    if !in_some_core(name) || core_tools(policy.mode).contains(&name) {
149        return Ok(());
150    }
151    Err(AxError::failure(
152        AxCode::GateDenied,
153        format!("run {name}"),
154        format!("{name} does not run in {} mode", policy.mode.as_str()),
155    )
156    .with_recovery("answer in the conversation, or ask the User to switch this run to work mode"))
157}
158
159/// The run policy in force for one run (`crates/runtime/spec/PolicyTake.lean`
160/// §8-62, runtime D28).
161///
162/// One writer and many readers. A change that reaches the run at any
163/// safe point waits in the cell, and the run's driver loop puts the
164/// last one in force at `SafePoint::BeforeWave` and nowhere else; the
165/// write gates hold a [`PolicyReader`] that they ask once per write. So
166/// every call of one wave is judged under one policy, the one in force
167/// when the wave began.
168#[derive(Debug)]
169pub struct PolicyCell {
170    shared: Arc<RwLock<RunPolicy>>,
171    arrived: Option<RunPolicy>,
172}
173
174impl PolicyCell {
175    /// The cell a run opens with, holding `run_started.policy`.
176    #[must_use]
177    pub fn new(start: RunPolicy) -> PolicyCell {
178        PolicyCell {
179            shared: Arc::new(RwLock::new(start)),
180            arrived: None,
181        }
182    }
183
184    /// A read-only view of the policy in force, for a write gate.
185    #[must_use]
186    pub fn reader(&self) -> PolicyReader {
187        PolicyReader {
188            shared: Arc::clone(&self.shared),
189        }
190    }
191
192    /// A `run_policy_changed` reached the run at a safe point. It waits
193    /// for the next `BeforeWave`; a later arrival overrides it.
194    pub(crate) fn arrive(&mut self, policy: RunPolicy) {
195        self.arrived = Some(policy);
196    }
197
198    /// At `SafePoint::BeforeWave`: puts the last arrival in force and
199    /// hands it back so the driver can append the note that tells the
200    /// model; `None` when nothing arrived, and then nothing is appended.
201    pub(crate) fn take_at_wave(&mut self) -> Option<RunPolicy> {
202        let taken = self.arrived.take()?;
203        // A poisoned lock still holds a whole policy: the only write is
204        // the assignment of a `Copy` value, which cannot stop halfway.
205        *self.shared.write().unwrap_or_else(PoisonError::into_inner) = taken;
206        Some(taken)
207    }
208}
209
210/// What a write gate reads: the policy in force, never a change that
211/// has arrived and not yet been taken.
212#[derive(Debug, Clone)]
213pub struct PolicyReader {
214    shared: Arc<RwLock<RunPolicy>>,
215}
216
217impl PolicyReader {
218    /// The policy in force now; asked once per write.
219    #[must_use]
220    pub fn now(&self) -> RunPolicy {
221        *self.shared.read().unwrap_or_else(PoisonError::into_inner)
222    }
223}
224
225/// The note appended after a wave's results when a change was taken. It
226/// is the only place a run's write limit is spelled to the model, so the
227/// frozen prefix and the tool descriptions stay byte for byte as they
228/// were sent (§8-62).
229#[must_use]
230pub(crate) fn policy_note(policy: &RunPolicy) -> String {
231    format!(
232        "The User changed this run's policy; from the next tool call on: mode {}, write {}, \
233         admission {}, landing {}.",
234        policy.mode.as_str(),
235        policy.write.as_str(),
236        policy.admit.as_str(),
237        policy.landing.as_str()
238    )
239}
240
241/// What a run has to show for itself.
242///
243/// `None` is not `Some(false)`: a suite that was never run and a suite
244/// that failed are different facts, and a requirement that treated them
245/// alike would let "we did not check" pass as "we checked and it was
246/// fine".
247#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
248pub struct Produced {
249    /// The asset's own tests ran and passed.
250    pub tests_passed: Option<bool>,
251    /// The observable contract moved under the renovation.
252    pub contract_moved: bool,
253    /// Held-in evidence: it did not get worse on what it was built from.
254    pub held_in: Option<bool>,
255    /// Held-out evidence: it stands up away from what it was built from.
256    pub held_out: Option<bool>,
257}
258
259/// Whether this may land, and if not, what to do about it.
260#[derive(Debug, Clone, Copy, PartialEq, Eq)]
261pub enum Admission {
262    Lands,
263    Refused {
264        because: &'static str,
265        alternative: &'static str,
266    },
267}
268
269/// Whether what a run produced may be merged, under the policy it was
270/// dispatched with (`crates/runtime/spec/Mode.lean` §8-54).
271///
272/// The landing policy is asked first: an experiment lands nothing
273/// however well it went. Then the evidence requirement, exhaustively,
274/// so a new requirement has to say what it demands. The mode takes no
275/// part: talk and work produce things that meet the same merge.
276#[must_use]
277pub fn admits(policy: &RunPolicy, produced: &Produced) -> Admission {
278    match policy.landing {
279        LandingPolicy::Experiment => Admission::Refused {
280            because: "nothing produced in an experiment lands",
281            alternative: "write what you learned into Memo.md, then ask for the work again \
282                          with the ordinary landing",
283        },
284        LandingPolicy::Ordinary => admits_evidence(policy.admit, produced),
285    }
286}
287
288/// The evidence half of [`admits`].
289///
290/// `Standing` adds nothing: the building's own checks were made where
291/// they are made. `Tested` wants the asset proven by its own tests.
292/// `ContractKept` wants the contract to have stayed where it was,
293/// because a renovation that moves it is not a renovation.
294/// `DoubleValidated` wants both halves of the double validation: it is
295/// asked for a change to how the city behaves, so confidence is not the
296/// currency — evidence is.
297fn admits_evidence(required: AdmissionRequirement, produced: &Produced) -> Admission {
298    match required {
299        AdmissionRequirement::Standing => Admission::Lands,
300        AdmissionRequirement::Tested => match produced.tests_passed {
301            Some(true) => Admission::Lands,
302            Some(false) => Admission::Refused {
303                because: "the asset's own tests did not pass",
304                alternative: "fix the asset or the test, then offer it again",
305            },
306            None => Admission::Refused {
307                because: "the asset has no tests of its own",
308                alternative: "write the test that would fail if this asset broke",
309            },
310        },
311        AdmissionRequirement::ContractKept => {
312            if produced.contract_moved {
313                Admission::Refused {
314                    because: "the asset's observable contract moved",
315                    alternative: "keep the contract and renovate behind it, or ask for the work \
316                                  again under double_validated with held-out evidence",
317                }
318            } else {
319                Admission::Lands
320            }
321        }
322        AdmissionRequirement::DoubleValidated => match (produced.held_in, produced.held_out) {
323            (Some(true), Some(true)) => Admission::Lands,
324            (Some(false), _) => Admission::Refused {
325                because: "it got worse on the held-in set",
326                alternative: "a change that costs more than it buys is not adopted; revise it",
327            },
328            (_, Some(false)) => Admission::Refused {
329                because: "it did not stand up on the held-out set",
330                alternative: "a gain that only shows where it was built is a gain in fitting, \
331                              not in ability",
332            },
333            _ => Admission::Refused {
334                because: "one half of the double validation is missing",
335                alternative: "run the suite on both sets; an unmeasured change is not adopted on \
336                              confidence",
337            },
338        },
339    }
340}
341
342#[cfg(test)]
343#[allow(
344    clippy::unwrap_used,
345    clippy::expect_used,
346    clippy::panic,
347    reason = "test code"
348)]
349mod tests {
350    use super::*;
351    use proptest::prelude::*;
352
353    /// One thing a run meets, as `crates/runtime/spec/PolicyTake.lean`
354    /// names it: a change reaching the run, a `BeforeWave`, or one call of
355    /// the wave asking a write gate.
356    #[derive(Debug, Clone, Copy)]
357    enum Step {
358        Change(RunPolicy),
359        Wave,
360        Call,
361    }
362
363    fn any_policy() -> impl Strategy<Value = RunPolicy> {
364        (
365            prop::sample::select(Mode::ALL.to_vec()),
366            prop::sample::select(kernel::WriteLimit::ALL.to_vec()),
367            prop::sample::select(AdmissionRequirement::ALL.to_vec()),
368            prop::sample::select(LandingPolicy::ALL.to_vec()),
369        )
370            .prop_map(|(mode, write, admit, landing)| RunPolicy {
371                mode,
372                write,
373                admit,
374                landing,
375            })
376    }
377
378    fn any_step() -> impl Strategy<Value = Step> {
379        prop_oneof![
380            any_policy().prop_map(Step::Change),
381            Just(Step::Wave),
382            Just(Step::Call),
383        ]
384    }
385
386    /// The model's two properties over every trace: a wave's calls all
387    /// read the policy in force when the wave began, and a `BeforeWave`
388    /// takes the last change that arrived before it, and only then.
389    fn walk(start: RunPolicy, trace: &[Step]) -> Result<(), TestCaseError> {
390        let mut cell = PolicyCell::new(start);
391        let gate = cell.reader();
392        let mut in_force = start;
393        let mut last_arrival = None;
394        for step in trace {
395            match *step {
396                Step::Change(policy) => {
397                    cell.arrive(policy);
398                    last_arrival = Some(policy);
399                }
400                Step::Wave => {
401                    let taken = cell.take_at_wave();
402                    prop_assert_eq!(taken, last_arrival.take());
403                    in_force = taken.unwrap_or(in_force);
404                }
405                Step::Call => prop_assert_eq!(gate.now(), in_force),
406            }
407        }
408        Ok(())
409    }
410
411    proptest! {
412        #[test]
413        fn policy_take_holds_on_every_trace(
414            start in any_policy(),
415            trace in prop::collection::vec(any_step(), 0..24),
416        ) {
417            walk(start, &trace)?;
418        }
419    }
420
421    /// The model's counterexample to reading the mailslot
422    /// (`eager_reading_splits_a_wave`), kept as the trace that bit.
423    #[test]
424    fn a_change_inside_a_wave_leaves_that_wave_alone() {
425        let start = RunPolicy::of(Mode::Work);
426        let tighter = RunPolicy {
427            write: kernel::WriteLimit::Create,
428            ..start
429        };
430        walk(start, &[Step::Call, Step::Change(tighter), Step::Call]).unwrap();
431    }
432
433    /// The tool list is the same in every mode, so the mode in force is
434    /// asked at the call: a chat run creates nothing (runtime D25).
435    #[test]
436    fn a_chat_run_is_refused_an_edit_and_the_disk_is_untouched() {
437        let tmp = tempfile::tempdir().unwrap();
438        let work = kernel::Address::parse("work").unwrap();
439        std::fs::create_dir_all(tmp.path().join("work")).unwrap();
440        let tool = crate::tools::EditTool::new(
441            tmp.path(),
442            work.clone(),
443            kernel::WriteDomain::new(vec![work]).unwrap(),
444            crate::PolicyCell::new(kernel::RunPolicy::of(kernel::Mode::Chat)).reader(),
445        )
446        .unwrap();
447        let refused = kernel::Tool::invoke(&tool, &edit_call());
448        assert_eq!(
449            refused.err().map(|err| *err.code()),
450            Some(AxCode::GateDenied)
451        );
452        assert!(!tmp.path().join("work/new.md").exists());
453    }
454
455    fn edit_call() -> kernel::ToolCall {
456        let args = serde_json::json!({
457            "path": "work/new.md", "base_version": "new", "old": "", "new": "text",
458        });
459        kernel::ToolCall {
460            id: "call-1".to_owned(),
461            name: kernel::ToolName::parse("edit").unwrap(),
462            args: kernel::Payload::of(&args).unwrap(),
463        }
464    }
465
466    fn work(admit: AdmissionRequirement) -> RunPolicy {
467        RunPolicy {
468            admit,
469            ..RunPolicy::of(Mode::Work)
470        }
471    }
472
473    /// A requirement chosen is not evidence held: work that asked for
474    /// its own tests and ran none does not land.
475    #[test]
476    fn a_work_run_without_the_evidence_it_chose_does_not_land() {
477        let Admission::Refused { because, .. } =
478            admits(&work(AdmissionRequirement::Tested), &Produced::default())
479        else {
480            panic!("work that chose `tested` and ran no test landed");
481        };
482        assert!(because.contains("no tests"), "{because}");
483    }
484
485    /// A chat run is told one thing, to talk with the person.
486    #[test]
487    fn chat_is_one_line_about_the_conversation() {
488        let entry = catalog_entry(Mode::Chat);
489        assert_eq!(entry.name, "mode:chat");
490        assert!(entry.disclosure.contains("convers"), "{}", entry.disclosure);
491        assert!(!entry.disclosure.contains('\n'), "one line");
492        assert!(
493            !entry.expansion.is_empty(),
494            "a read of the entry says something"
495        );
496        assert_eq!(catalog_entry(Mode::Work).name, "mode:work");
497    }
498
499    /// The building's own checks are made where they are made; the
500    /// standing requirement adds none, in either mode.
501    #[test]
502    fn standing_adds_nothing_in_either_mode() {
503        for mode in Mode::ALL {
504            assert_eq!(
505                admits(&RunPolicy::of(mode), &Produced::default()),
506                Admission::Lands
507            );
508        }
509    }
510
511    #[test]
512    fn tested_wants_the_asset_proven_and_says_which_way_it_failed() {
513        let policy = work(AdmissionRequirement::Tested);
514        let failed = Produced {
515            tests_passed: Some(false),
516            ..Produced::default()
517        };
518        let Admission::Refused { because, .. } = admits(&policy, &failed) else {
519            panic!("a failing asset does not land");
520        };
521        assert!(
522            because.contains("did not pass"),
523            "not the untested sentence"
524        );
525        let passed = Produced {
526            tests_passed: Some(true),
527            ..Produced::default()
528        };
529        assert_eq!(admits(&policy, &passed), Admission::Lands);
530    }
531
532    #[test]
533    fn contract_kept_refuses_a_renovation_that_moved_the_contract() {
534        let policy = work(AdmissionRequirement::ContractKept);
535        assert_eq!(admits(&policy, &Produced::default()), Admission::Lands);
536        let moved = Produced {
537            contract_moved: true,
538            ..Produced::default()
539        };
540        let Admission::Refused { alternative, .. } = admits(&policy, &moved) else {
541            panic!("a moved contract is not a renovation");
542        };
543        assert!(
544            alternative.contains("double_validated"),
545            "the refusal names the requirement that would take it"
546        );
547    }
548
549    #[test]
550    fn double_validated_takes_nothing_on_confidence() {
551        let policy = work(AdmissionRequirement::DoubleValidated);
552        let both = Produced {
553            held_in: Some(true),
554            held_out: Some(true),
555            ..Produced::default()
556        };
557        assert_eq!(admits(&policy, &both), Admission::Lands);
558        for missing in [
559            Produced {
560                held_in: Some(true),
561                ..Produced::default()
562            },
563            Produced {
564                held_out: Some(true),
565                ..Produced::default()
566            },
567            Produced::default(),
568        ] {
569            assert!(
570                matches!(admits(&policy, &missing), Admission::Refused { .. }),
571                "half of a double validation is not a double validation"
572            );
573        }
574        let regressed = Produced {
575            held_in: Some(true),
576            held_out: Some(false),
577            ..Produced::default()
578        };
579        let Admission::Refused { because, .. } = admits(&policy, &regressed) else {
580            panic!("a change that only holds where it was built does not land");
581        };
582        assert!(because.contains("held-out"));
583    }
584
585    /// An experiment lands nothing, whatever it proved and whatever it
586    /// was allowed to write.
587    #[test]
588    fn an_experiment_lands_nothing_however_well_it_went() {
589        let excellent = Produced {
590            tests_passed: Some(true),
591            contract_moved: false,
592            held_in: Some(true),
593            held_out: Some(true),
594        };
595        for admit in AdmissionRequirement::ALL {
596            let policy = RunPolicy {
597                landing: LandingPolicy::Experiment,
598                write: kernel::WriteLimit::Create,
599                ..work(admit)
600            };
601            assert!(matches!(
602                admits(&policy, &excellent),
603                Admission::Refused { .. }
604            ));
605        }
606    }
607}