kernel/
write_domain.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//! WriteDomain prefix checking and edit-war detection. C17 is enforced twice on purpose: a reserved prefix cannot be
7//! *constructed into* a domain, and a reserved target is refused at
8//! judgment even so — fail-closed has no single point of failure.
9//! The part `crates/kernel/spec/WriteDomain.lean` specifies this module.
10
11use std::collections::BTreeMap;
12
13use serde::{Deserialize, Serialize};
14
15use crate::address::Address;
16use crate::consts_policy::EDIT_WAR_FREEZE;
17use crate::error::{AxCode, AxError};
18use crate::event::RunId;
19
20/// A validated set of prefixes.
21///
22/// The one construction point C17 is enforced at, and the reason
23/// [`WriteDomain`] can be an enum with public variants without gaining a
24/// second way in: a variant is spellable, but only with a value that has
25/// already been checked.
26#[derive(Debug, Clone, PartialEq, Eq)]
27pub struct DomainPrefixes {
28    prefixes: Vec<Address>,
29}
30
31impl DomainPrefixes {
32    /// C17 at the construction point: any member under the reserved
33    /// prefix refuses the whole set. An empty set is legal (a read-only
34    /// actor writes nowhere).
35    ///
36    /// # Errors
37    /// `E_INVALID_ARGS` naming the reserved member.
38    pub fn new(prefixes: Vec<Address>) -> Result<DomainPrefixes, AxError> {
39        if let Some(reserved) = prefixes.iter().find(|p| p.is_reserved()) {
40            return Err(AxError::failure(
41                AxCode::InvalidArgs,
42                "construct write domain",
43                reserved.as_str(),
44            )
45            .with_recovery(
46                "the reserved prefix is outside every write domain (C17); \
47                 drop it from the prefix set",
48            ));
49        }
50        Ok(DomainPrefixes { prefixes })
51    }
52
53    pub fn iter(&self) -> impl Iterator<Item = &Address> {
54        self.prefixes.iter()
55    }
56}
57
58/// The set of prefixes one actor may write under, and what it may write
59/// inside them.
60///
61/// Exhaustive rather than a set plus a flag: "every file here" and "the
62/// Markdown documents here" are two policies, and the second one is what
63/// City Hall's residents are given so that a planner which may not build
64/// is a type rather than a sentence in a prompt.
65#[derive(Debug, Clone, PartialEq, Eq)]
66pub enum WriteDomain {
67    /// Every file under the prefixes.
68    Everything(DomainPrefixes),
69    /// Markdown documents under the prefixes, and never a plan file:
70    /// `Roadmap.md` has one editing entrance, and it is the `plan` tool.
71    Documents(DomainPrefixes),
72}
73
74impl WriteDomain {
75    /// The ordinary domain: every file under these prefixes.
76    ///
77    /// # Errors
78    /// Propagates [`DomainPrefixes::new`].
79    pub fn new(prefixes: Vec<Address>) -> Result<WriteDomain, AxError> {
80        Ok(WriteDomain::Everything(DomainPrefixes::new(prefixes)?))
81    }
82
83    /// The documents-only domain.
84    ///
85    /// # Errors
86    /// Propagates [`DomainPrefixes::new`].
87    pub fn documents(prefixes: Vec<Address>) -> Result<WriteDomain, AxError> {
88        Ok(WriteDomain::Documents(DomainPrefixes::new(prefixes)?))
89    }
90
91    pub fn prefixes(&self) -> impl Iterator<Item = &Address> {
92        match self {
93            WriteDomain::Everything(set) | WriteDomain::Documents(set) => set.iter(),
94        }
95    }
96
97    /// Whether a declared area lies inside this domain at all: the
98    /// prefix half of [`admits`](Self::admits), for the subject that
99    /// has no file name. A tool declares the room it works in, and a
100    /// room is neither Markdown nor code.
101    #[must_use]
102    pub fn reaches(&self, area: &Address) -> bool {
103        !area.is_reserved() && self.prefixes().any(|p| area.is_within(p))
104    }
105
106    /// The domain door's primitive. Reserved targets are Outside no
107    /// matter what the set says, and a documents domain answers a third
108    /// way: inside the prefixes, and still not a file it writes.
109    pub fn admits(&self, target: &Address) -> DomainVerdict {
110        if !self.reaches(target) {
111            return DomainVerdict::Outside {
112                prefixes: self.prefix_strings(),
113            };
114        }
115        match self {
116            WriteDomain::Everything(_) => DomainVerdict::Within,
117            WriteDomain::Documents(_) => document_verdict(target),
118        }
119    }
120
121    fn prefix_strings(&self) -> Vec<String> {
122        self.prefixes().map(|p| p.as_str().to_owned()).collect()
123    }
124}
125
126/// What a run may do to a file that already exists inside its write
127/// domain (`crates/kernel/spec/WriteDomain.lean` §8-78).
128///
129/// It narrows the domain and never widens it: the domain answers where
130/// a run may write and what kind of file, this answers whether a write
131/// may change a file that is already there. Whether the target exists
132/// is the filesystem's fact at the moment of the write, so the check
133/// that makes `Create` hold is the writer's atomic create; the rule and
134/// its refusal are [`crate::gate::replacing`].
135#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
136#[serde(rename_all = "snake_case")]
137#[cfg_attr(feature = "schema", derive(schemars::JsonSchema))]
138pub enum WriteLimit {
139    /// No narrowing beyond the write domain.
140    Full,
141    /// Create files that do not exist; change, remove and rename none,
142    /// including one this run created itself.
143    Create,
144}
145
146impl WriteLimit {
147    /// Both limits, the one that narrows nothing first.
148    pub const ALL: [WriteLimit; 2] = [WriteLimit::Full, WriteLimit::Create];
149
150    /// The word this limit travels under.
151    #[must_use]
152    pub const fn as_str(self) -> &'static str {
153        match self {
154            WriteLimit::Full => "full",
155            WriteLimit::Create => "create",
156        }
157    }
158}
159
160/// The last segment of an address: its file name.
161fn file_name(target: &Address) -> &str {
162    let raw = target.as_str();
163    raw.rsplit('/').next().unwrap_or(raw)
164}
165
166/// What a documents domain says about one target already known to be
167/// inside its prefixes.
168fn document_verdict(target: &Address) -> DomainVerdict {
169    let name = file_name(target);
170    if name == crate::spine::ROADMAP_FILE {
171        return DomainVerdict::NotWritable {
172            reason: DocumentReason::ThePlan,
173        };
174    }
175    if name.ends_with(".md") {
176        DomainVerdict::Within
177    } else {
178        DomainVerdict::NotWritable {
179            reason: DocumentReason::NotMarkdown,
180        }
181    }
182}
183
184/// Deliberately exhaustive verdict; `prefixes` feeds the refusal's
185/// nearby list.
186#[derive(Debug, Clone, PartialEq, Eq)]
187pub enum DomainVerdict {
188    Within,
189    Outside {
190        prefixes: Vec<String>,
191    },
192    /// Inside the prefixes, and still not a file this domain writes.
193    NotWritable {
194        reason: DocumentReason,
195    },
196}
197
198/// Why a documents domain refuses a target that is inside its prefixes.
199#[derive(Debug, Clone, Copy, PartialEq, Eq)]
200pub enum DocumentReason {
201    /// Not a Markdown document.
202    NotMarkdown,
203    /// The plan file, whose one editing entrance is the `plan` tool.
204    ThePlan,
205}
206
207/// One observed write, in time order (slice order is the clock).
208#[derive(Debug, Clone, PartialEq, Eq)]
209pub struct EditSample {
210    pub addr: Address,
211    pub run: RunId,
212}
213
214#[derive(Debug, Clone, PartialEq, Eq)]
215pub enum EditWarVerdict {
216    Calm,
217    Freeze { addr: Address },
218}
219
220/// Edit-war detection: a "reclaim" is run X editing a
221/// file back after run Y took it (X, Y, X). Reclaims at or over
222/// `EDIT_WAR_FREEZE` freeze that file. Per-address, deterministic:
223/// addresses are examined in BTreeMap order, first hit wins.
224pub fn observe_edit_war(samples: &[EditSample]) -> EditWarVerdict {
225    let mut per_addr: BTreeMap<&Address, Vec<RunId>> = BTreeMap::new();
226    for sample in samples {
227        let runs = per_addr.entry(&sample.addr).or_default();
228        if runs.last() != Some(&sample.run) {
229            runs.push(sample.run);
230        }
231    }
232    for (addr, runs) in per_addr {
233        let mut reclaims: u32 = 0;
234        for i in 2..runs.len() {
235            let (Some(now), Some(prev), Some(before)) = (
236                runs.get(i),
237                runs.get(i.wrapping_sub(1)),
238                runs.get(i.wrapping_sub(2)),
239            ) else {
240                continue;
241            };
242            if now == before && now != prev {
243                reclaims = reclaims.saturating_add(1);
244            }
245        }
246        if reclaims >= EDIT_WAR_FREEZE {
247            return EditWarVerdict::Freeze { addr: addr.clone() };
248        }
249    }
250    EditWarVerdict::Calm
251}
252
253// No kani harness lives here. Every value this module judges is an
254// `Address`, which owns a `String`, so a symbolic harness would hand
255// CBMC loops it cannot bound, and a harness over one fixed address
256// would restate the test below at a higher price (`crates/kernel/Spec.lean`
257// §2).
258
259#[cfg(test)]
260#[allow(
261    clippy::unwrap_used,
262    clippy::expect_used,
263    clippy::panic,
264    clippy::indexing_slicing,
265    clippy::wildcard_enum_match_arm,
266    clippy::let_underscore_must_use,
267    clippy::let_underscore_untyped,
268    reason = "test code"
269)]
270mod tests {
271    use super::*;
272
273    fn addr(raw: &str) -> Address {
274        Address::parse(raw).unwrap()
275    }
276
277    fn run(n: u8) -> RunId {
278        RunId::parse(&format!("0198f6a2-7c4a-7bbb-9d1e-0000000000{n:02x}")).unwrap()
279    }
280
281    #[test]
282    fn a_reserved_member_refuses_the_whole_domain() {
283        let err = WriteDomain::new(vec![addr("b"), addr(".sprawling/cas")]).unwrap_err();
284        assert_eq!(err.code(), &AxCode::InvalidArgs);
285    }
286
287    #[test]
288    fn admits_within_and_refuses_outside_with_nearby() {
289        let domain = WriteDomain::new(vec![addr("b1/room"), addr("b2")]).unwrap();
290        assert_eq!(
291            domain.admits(&addr("b1/room/file.md")),
292            DomainVerdict::Within
293        );
294        assert_eq!(domain.admits(&addr("b2")), DomainVerdict::Within);
295        match domain.admits(&addr("b3/x")) {
296            DomainVerdict::Outside { prefixes } => {
297                assert_eq!(prefixes, ["b1/room", "b2"]);
298            }
299            other => panic!("b3/x is outside, not {other:?}"),
300        }
301    }
302
303    #[test]
304    fn reserved_target_is_outside_even_for_an_empty_domain() {
305        let domain = WriteDomain::new(vec![]).unwrap();
306        assert!(matches!(
307            domain.admits(&addr(".sprawling/config")),
308            DomainVerdict::Outside { .. }
309        ));
310        assert!(matches!(
311            domain.admits(&addr("anywhere")),
312            DomainVerdict::Outside { .. }
313        ));
314    }
315
316    #[test]
317    fn two_full_reclaims_freeze_the_file() {
318        let file = addr("b/contested.md");
319        let samples: Vec<EditSample> = [run(1), run(2), run(1), run(2)]
320            .into_iter()
321            .map(|r| EditSample {
322                addr: file.clone(),
323                run: r,
324            })
325            .collect();
326        assert_eq!(
327            observe_edit_war(&samples),
328            EditWarVerdict::Freeze { addr: file }
329        );
330    }
331
332    #[test]
333    fn one_reclaim_or_same_run_bursts_stay_calm() {
334        let file = addr("b/f.md");
335        let one_reclaim: Vec<EditSample> = [run(1), run(2), run(1)]
336            .into_iter()
337            .map(|r| EditSample {
338                addr: file.clone(),
339                run: r,
340            })
341            .collect();
342        assert_eq!(observe_edit_war(&one_reclaim), EditWarVerdict::Calm);
343        // Consecutive edits by the same run collapse: no alternation, no war.
344        let bursts: Vec<EditSample> = [run(1), run(1), run(2), run(2), run(1), run(1)]
345            .into_iter()
346            .map(|r| EditSample {
347                addr: file.clone(),
348                run: r,
349            })
350            .collect();
351        assert_eq!(observe_edit_war(&bursts), EditWarVerdict::Calm);
352    }
353
354    /// A file passed on from run to run, none of them taking it back, is
355    /// work handed along rather than a war.
356    #[test]
357    fn a_file_handed_along_without_a_reclaim_stays_calm() {
358        let file = addr("b/relay.md");
359        let relay: Vec<EditSample> = (1..=6)
360            .map(|n| EditSample {
361                addr: file.clone(),
362                run: run(n),
363            })
364            .collect();
365        assert_eq!(observe_edit_war(&relay), EditWarVerdict::Calm);
366    }
367
368    #[test]
369    fn wars_are_per_address_not_global() {
370        let samples: Vec<EditSample> = [
371            (addr("b/one.md"), run(1)),
372            (addr("b/two.md"), run(2)),
373            (addr("b/one.md"), run(2)),
374            (addr("b/two.md"), run(1)),
375            (addr("b/one.md"), run(1)),
376            (addr("b/two.md"), run(2)),
377        ]
378        .into_iter()
379        .map(|(a, r)| EditSample { addr: a, run: r })
380        .collect();
381        // Each file saw only one reclaim; interleaving does not add up.
382        assert_eq!(observe_edit_war(&samples), EditWarVerdict::Calm);
383    }
384}
kernel/write_domain.rs

kernel/
write_domain.rs
