kernel/
repair.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//! Repair leases: when the environment itself is
7//! broken, repair is serialized — one live lease per scope subtree, so
8//! two runs can never "fix" the same breakage into a bigger one. The
9//! active table is the caller's state; kernel only judges.
10//! The part `crates/kernel/spec/Repair.lean` specifies this module.
11
12use std::collections::BTreeMap;
13
14use crate::address::Address;
15use crate::event::RunId;
16
17/// Deliberately exhaustive verdict. Queued is a legal outcome, not an
18/// error — E_REPAIR_BUSY only carries it across the tool surface.
19#[derive(Debug, Clone, PartialEq, Eq)]
20pub enum RepairVerdict {
21    Lease,
22    Queued { holder: RunId },
23}
24
25/// Overlap either way queues (same rule as goal resources); the same
26/// holder re-requesting its exact scope re-leases (idempotent recovery).
27/// First overlapping holder wins the report, in BTreeMap order.
28pub fn request(active: &BTreeMap<Address, RunId>, scope: &Address, who: &RunId) -> RepairVerdict {
29    for (held, holder) in active {
30        let overlaps = scope.is_within(held) || held.is_within(scope);
31        if !overlaps {
32            continue;
33        }
34        if held == scope && holder == who {
35            return RepairVerdict::Lease;
36        }
37        return RepairVerdict::Queued { holder: *holder };
38    }
39    RepairVerdict::Lease
40}
41
42#[cfg(test)]
43#[allow(
44    clippy::unwrap_used,
45    clippy::expect_used,
46    clippy::panic,
47    clippy::indexing_slicing,
48    reason = "test code"
49)]
50mod tests {
51    use super::*;
52
53    fn addr(raw: &str) -> Address {
54        Address::parse(raw).unwrap()
55    }
56
57    fn run(n: u8) -> RunId {
58        RunId::parse(&format!("0198f6a2-7c4a-7bbb-9d1e-0000000000{n:02x}")).unwrap()
59    }
60
61    #[test]
62    fn a_free_scope_leases() {
63        let active = BTreeMap::new();
64        assert_eq!(
65            request(&active, &addr("b/env"), &run(1)),
66            RepairVerdict::Lease
67        );
68    }
69
70    #[test]
71    fn overlap_queues_either_way_and_names_the_holder() {
72        let mut active = BTreeMap::new();
73        active.insert(addr("b/env"), run(1));
74        assert_eq!(
75            request(&active, &addr("b/env/tools"), &run(2)),
76            RepairVerdict::Queued { holder: run(1) }
77        );
78        assert_eq!(
79            request(&active, &addr("b"), &run(2)),
80            RepairVerdict::Queued { holder: run(1) }
81        );
82        assert_eq!(
83            request(&active, &addr("other"), &run(2)),
84            RepairVerdict::Lease
85        );
86    }
87
88    #[test]
89    fn the_holder_re_requesting_its_exact_scope_re_leases() {
90        let mut active = BTreeMap::new();
91        active.insert(addr("b/env"), run(1));
92        assert_eq!(
93            request(&active, &addr("b/env"), &run(1)),
94            RepairVerdict::Lease
95        );
96        // But a narrower scope by the same holder still queues: one lease,
97        // one scope — narrowing is a release-and-reacquire, not a nest.
98        assert_eq!(
99            request(&active, &addr("b/env/x"), &run(1)),
100            RepairVerdict::Queued { holder: run(1) }
101        );
102    }
103}
kernel/repair.rs

kernel/
repair.rs
