kernel/tool/
writes.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//! What a call that ran may have written to the city's tree, as its tool
7//! can tell (`crates/kernel/spec/Tool.lean` §8-23).
8
9use super::Effect;
10use crate::Address;
11
12/// What one call, or every call since the last checkpoint, may have written.
13///
14/// A checkpoint stages what this names (`crates/runtime/Spec.lean` §8-45), so an
15/// answer narrower than the truth leaves a write no commit carries. Only
16/// a tool that knows every file it wrote answers `Paths`.
17#[derive(Debug, Clone, PartialEq, Eq)]
18pub enum Writes {
19    /// Nothing in the tree.
20    Nothing,
21    /// Exactly these files.
22    Paths(Vec<Address>),
23    /// Somewhere in the run's write domain, which the checkpoint then walks.
24    Domain,
25}
26
27impl Writes {
28    /// The default answer, read off the declared effect alone: only a
29    /// `Read` promises to leave the tree alone, and every other effect -
30    /// a command, a desk, a rule change, a spawned worktree - may write
31    /// where no argument says.
32    pub fn of(effect: &Effect) -> Self {
33        match effect {
34            Effect::Read => Self::Nothing,
35            Effect::Write { .. }
36            | Effect::Egress
37            | Effect::Connector { .. }
38            | Effect::Spawn
39            | Effect::Govern
40            | Effect::AttachUserBrowser { .. }
41            | Effect::Spend => Self::Domain,
42        }
43    }
44
45    /// Both answers at once: `Domain` absorbs everything, `Nothing` adds
46    /// nothing, and two sets of paths join without duplicates.
47    #[must_use]
48    pub fn and(self, other: Self) -> Self {
49        match (self, other) {
50            (Self::Domain, _) | (_, Self::Domain) => Self::Domain,
51            (Self::Nothing, only) | (only, Self::Nothing) => only,
52            (Self::Paths(mut these), Self::Paths(those)) => {
53                for path in those {
54                    if !these.contains(&path) {
55                        these.push(path);
56                    }
57                }
58                Self::Paths(these)
59            }
60        }
61    }
62}
kernel/tool/writes.rs

kernel/tool/
writes.rs
