1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
// This Source Code Form is subject to the terms of the Mozilla Public
// License, v. 2.0. If a copy of the MPL was not distributed with this
// file, You can obtain one at https://mozilla.org/MPL/2.0/.
// Copyright (c) 2026 2youg1 and the sprawling contributors
//! Delegation: two delegate kinds, one level deep.
//! The guard is two-layered on purpose: statically, a `Delegate` value
//! has no delegate method — minting a grandchild cannot be spelled;
//! dynamically, `admit` re-checks depth at every spawn so a hand-rolled
//! path cannot sneak past the type. One level is an invariant, not a
//! constant — a constant would imply it is tunable.
//! The part `crates/kernel/spec/Delegation.lean` specifies this module.
use serde::{Deserialize, Serialize};
/// Resident delegates join society and answer for output; Ephemerals are
/// tools — one clarification channel up, nothing else.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
#[serde(rename_all = "snake_case")]
pub enum DelegateKind {
Resident,
Ephemeral,
}
impl DelegateKind {
/// The one spelling. Both the tool that parses these words and the
/// status line that prints them read it here, so a rename cannot
/// half-happen.
#[must_use]
pub fn as_str(self) -> &'static str {
match self {
DelegateKind::Resident => "resident",
DelegateKind::Ephemeral => "ephemeral",
}
}
}
/// The depth-zero position: the only type with a `delegate` method
/// (15.3-10). Who holds a `Delegator` is assembly's discipline; what a
/// `Delegate` value can mint is this module's — nothing.
#[derive(Debug)]
pub struct Delegator(());
impl Delegator {
/// Minting point: assembly and citysim only.
pub fn root() -> Delegator {
Delegator(())
}
pub fn delegate(&self, kind: DelegateKind) -> Delegate {
Delegate { kind }
}
}
/// A delegated position. No delegate method — the compile error is the
/// design (trybuild counterexample).
#[derive(Debug)]
pub struct Delegate {
kind: DelegateKind,
}
impl Delegate {
pub fn kind(&self) -> &DelegateKind {
&self.kind
}
}
/// Where a spawner stands.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum Depth {
Root,
Delegated,
}
/// Deliberately exhaustive verdict; the refusal (E_DELEGATION_DEPTH,
/// three parts) is shaped by gate::spawn — the sole gate-code producer.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum DelegationVerdict {
Allow,
Deny,
}
/// The dynamic half of the two-layer guard: a delegated position spawns
/// nothing, whatever kind it asks for.
pub fn admit(parent: Depth, kind: &DelegateKind) -> DelegationVerdict {
match parent {
Depth::Root => {
// Exhaustive on purpose: a new kind must decide its depth rule.
match kind {
DelegateKind::Resident | DelegateKind::Ephemeral => DelegationVerdict::Allow,
}
}
Depth::Delegated => DelegationVerdict::Deny,
}
}
#[cfg(test)]
#[allow(
clippy::unwrap_used,
clippy::expect_used,
clippy::panic,
clippy::indexing_slicing,
reason = "test code"
)]
mod tests {
use super::*;
#[test]
fn root_spawns_both_kinds_delegated_spawns_none() {
assert_eq!(
admit(Depth::Root, &DelegateKind::Resident),
DelegationVerdict::Allow
);
assert_eq!(
admit(Depth::Root, &DelegateKind::Ephemeral),
DelegationVerdict::Allow
);
assert_eq!(
admit(Depth::Delegated, &DelegateKind::Resident),
DelegationVerdict::Deny
);
assert_eq!(
admit(Depth::Delegated, &DelegateKind::Ephemeral),
DelegationVerdict::Deny
);
}
#[test]
fn the_static_path_mints_one_level_only() {
let root = Delegator::root();
let child = root.delegate(DelegateKind::Ephemeral);
assert_eq!(child.kind(), &DelegateKind::Ephemeral);
// `child.delegate(...)` does not compile — pinned by the
// trybuild case; this test documents the runtime-visible half.
}
}