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
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
//! The gate that ties blue's **closed capability universe** to the runtime it
//! describes — `theory/BLUE-EXECUTION.md` M0/M1.
//!
//! # Why this test lives here and not in `blue-lang-waku`
//!
//! `Capability`'s four host bundles claim to be exactly what
//! `blue_lang_runtime::sys` installs. A test inside `blue-lang-waku` could only
//! compare that claim against itself — the repo's named trap: *"a gate derived
//! from the thing it checks is a tautology."* So the evidence is taken from a
//! **real interpreter**: install the sys layer into a bare one, diff the
//! reserved head names before and after, and compare the difference against the
//! universe.
//!
//! It lives in `blue-lang-cli` because `blue-lang-cli` is the only crate that
//! turns the `sys` feature on, and without it there is no host layer to install.
//!
//! # What each gate would catch
//!
//! - a new sys primitive landing with no capability claiming it — a name a frame
//! could never grant and a program could therefore never legally call;
//! - a host name mis-filed under a **pure** bundle — which would put a host
//! effect inside a module that derives **zero imports**, the exact failure the
//! whole design exists to make impossible;
//! - a capability's bundle drifting away from the installer it names.
//!
//! # Red runs, recorded
//!
//! Each was performed on 2026-08-13, observed to fail, and reverted. Red runs
//! 1–3 (the closed type) are recorded in `blue_lang_waku::capability` and 4–5
//! (the derivation) in `blue_lang_waku::imports`.
//!
//! 6. **A sys name with no capability.** Deleting `"cwd"` from
//! `FILESYSTEM_NAMES` failed
//! `every_sys_name_is_claimed_by_exactly_one_host_capability` with
//! `sys installs names no capability grants: ["cwd"]` (2 tests red).
//! 7. **A host name filed as pure.** Moving `"read_file"` from
//! `FILESYSTEM_NAMES` into `COLLECTION_NAMES` failed
//! `no_pure_capability_grants_a_host_name` with ``collections grants
//! `read_file`, which the sys layer installs — a frame could name a host
//! effect and derive no import for it`` (3 tests red). **This is the
//! load-bearing red run**: the mutation is semantically meaningful — it
//! genuinely creates a host effect reachable through a frame that derives
//! zero imports — rather than a rename the gate cannot see.
//! 8. **The probe itself is not vacuous.** Removing the `install_sys_stdlib`
//! call from `sys_installed_names` failed `sys_installs_a_measurable_surface`
//! with `the sys layer installed 0 names; the floor is 37`, which is what
//! stops every "for every sys name…" assertion below from passing over an
//! empty set.
//! 9. **A bundle naming something the runtime does not install.** Adding
//! `"monotonic_now"` to `CLOCK_NAMES` failed
//! `every_host_capability_name_is_installed_by_the_sys_layer` with
//! ``clock grants `monotonic_now`, which the sys layer does not install``
//! — the direction red run 6 cannot reach, recorded separately because one
//! mutation proving one direction says nothing about the other.
use BTreeSet;
use Capability;
use Interpreter;
/// Every head name the host layer adds to an interpreter — **measured, by
/// installing it and diffing.**
///
/// `Interpreter::new()` is deliberately bare: no stdlib, no blue layers. The
/// difference is therefore exactly `install_sys_stdlib`'s contribution and
/// nothing else, which is what makes it independent evidence rather than a
/// restatement of a list.
/// Anti-vacuity, with the floor and the date: the host layer installs at least
/// 37 names as of 2026-08-13 (6 process, 20 filesystem, 4 environment,
/// 7 clock). Every gate below quantifies over this set.
/// **Every host primitive is claimed by exactly one host capability.**
///
/// The completeness direction: a sys name no capability grants is a name no
/// frame can permit, so a program calling it escapes its frame on a call the
/// runtime is perfectly willing to make.
/// **And every name a host capability grants is one the sys layer installs.**
///
/// The soundness direction. A bundle that named something the runtime does not
/// install would let a frame grant a capability that opens an import for a
/// function nobody can call — an import with no callee is exactly the kind of
/// stub `BLUE-EXECUTION.md` §0 says must not exist.
/// **No PURE capability grants a host name.**
///
/// The one that matters most. A pure bundle derives no import, so a host name
/// filed under one would be nameable inside a module whose import table is
/// empty — the design's central claim, inverted.
/// Every host capability's bundle is non-empty and its import is distinct.
///
/// Anti-vacuity for the two direction gates: both quantify over
/// `c.names()`, and both pass trivially over a bundle that grants nothing.
/// **`interpreter_hostless` is not hostless when the `sys` feature is on.**
///
/// Recorded as a measurement rather than left as a surprise. It forks a base
/// built by `interpreter(&mut ())`, and `interpreter` installs the sys layer
/// under `#[cfg(feature = "sys")]` — so in any build that turns the feature on
/// (this crate's, and every `cargo test --workspace` run through cargo's
/// feature unification) the "hostless" interpreter binds all 37 host
/// primitives.
///
/// Two documents credited the opposite. `blue-lang-pkg`'s `bluefile` module said
/// the manifest interpreter was *"safe by absence of a binding"*; it is safe by
/// the `check_reach` frame, which is a much narrower claim and the only true
/// one. This test is what makes the correction a measurement.
///
/// It asserts the CURRENT behaviour, so that changing it is a deliberate act
/// that fails here and gets a decision, rather than a quiet fix that leaves two
/// modules' docs describing different runtimes.