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
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
//! Proof for every advertised return shape.
//!
//! `shapes::DECLARED` may only contain shapes this file can reproduce by calling
//! the builtin. Two invariants keep it honest in both directions:
//!
//! * a declared shape with no probe, or one whose probe disagrees, fails; and
//! * a probe whose builtin is not declared fails.
//!
//! The second matters as much as the first. Without it a probe could be quietly
//! dropped when it became inconvenient, leaving a claim standing with nothing
//! behind it — which is exactly how the effect misclassifications survived.
use aethershell::shapes::{observe, DECLARED};
use aethershell::value::Value;
use std::collections::BTreeMap;
fn rec(pairs: &[(&str, Value)]) -> Value {
let mut m = BTreeMap::new();
for (k, v) in pairs {
m.insert(k.to_string(), v.clone());
}
Value::Record(m)
}
/// Call a builtin, returning `None` if it errors. A probe that cannot run is a
/// failed proof, not a skipped one.
fn call(name: &str, args: Vec<Value>) -> Option<Value> {
let mut env = aethershell::env::Env::new();
aethershell::builtins::call(name, args, &mut env).ok()
}
/// The probe set: a builtin, and **several** argument sets that exercise it
/// deterministically without touching the network, spawning a process, or
/// writing anything.
///
/// Every argument set must produce the *same* shape. That requirement is the
/// point of the plural: a combinator like `first` or `values` returns whatever
/// type it was handed, so a single probe would "prove" `array<int>` purely
/// because the test happened to pass integers. Varying the element type turns
/// that accident into a detectable disagreement, and an input-dependent shape
/// is then correctly refused rather than advertised as fixed.
///
/// Determinism decides membership. `platform_hostname` has a perfectly stable
/// shape, but proving it here would make the suite depend on an external
/// binary; such builtins stay undeclared until a probe can establish them
/// honestly.
fn probes() -> Vec<(&'static str, Vec<Vec<Value>>)> {
let table = Value::Array(vec![
rec(&[("n", Value::Int(1)), ("s", Value::Str("a".into()))]),
rec(&[("n", Value::Int(2)), ("s", Value::Str("b".into()))]),
]);
vec![
("pwd", vec![vec![]]),
(
"ls",
vec![vec![Value::Str(".".into())], vec![Value::Str("src".into())]],
),
(
"range",
vec![
vec![Value::Int(1), Value::Int(4)],
vec![Value::Int(0), Value::Int(2)],
],
),
(
"len",
vec![
vec![Value::Array(vec![Value::Int(1), Value::Int(2)])],
vec![Value::Array(vec![Value::Str("a".into())])],
],
),
(
"keys",
vec![
vec![rec(&[("a", Value::Int(1)), ("b", Value::Int(2))])],
vec![rec(&[("z", Value::Str("s".into()))])],
],
),
(
"values",
vec![
vec![rec(&[("a", Value::Int(1))])],
vec![rec(&[("a", Value::Str("s".into()))])],
],
),
(
"upper",
vec![
vec![Value::Str("ab".into())],
vec![Value::Str("xyz".into())],
],
),
(
"split",
vec![
vec![Value::Str("a,b,c".into()), Value::Str(",".into())],
vec![Value::Str("a b".into()), Value::Str(" ".into())],
],
),
(
"aecon",
vec![
vec![table.clone()],
vec![Value::Array(vec![rec(&[("x", Value::Bool(true))])])],
],
),
(
"tokens",
vec![
vec![Value::Str("hello world".into())],
vec![Value::Str("a".into())],
],
),
(
"type_of",
vec![
vec![Value::Int(1)],
vec![Value::Str("s".into())],
vec![Value::Bool(true)],
],
),
(
"sum",
vec![
vec![Value::Array(vec![Value::Int(1), Value::Int(2)])],
vec![Value::Array(vec![Value::Float(1.5), Value::Float(2.5)])],
],
),
(
"unique",
vec![
vec![Value::Array(vec![Value::Int(1), Value::Int(1)])],
vec![Value::Array(vec![
Value::Str("a".into()),
Value::Str("a".into()),
])],
],
),
(
"first",
vec![
vec![Value::Array(vec![Value::Int(1), Value::Int(2)])],
vec![Value::Array(vec![Value::Str("a".into())])],
],
),
(
"reverse",
vec![
vec![Value::Array(vec![Value::Int(1), Value::Int(2)])],
vec![Value::Array(vec![
Value::Str("a".into()),
Value::Str("b".into()),
])],
],
),
("ontology_manifest", vec![vec![]]),
]
}
/// Observe a builtin across all its argument sets. Returns the agreed shape, or
/// an explanation of why no shape can be advertised.
fn agreed_shape(name: &str, arg_sets: &[Vec<Value>]) -> Result<String, String> {
let mut seen: Vec<String> = Vec::new();
for args in arg_sets {
match call(name, args.clone()) {
None => return Err(format!("{name}: probe errored")),
Some(v) => {
let s = observe(&v);
if !seen.contains(&s) {
seen.push(s);
}
}
}
}
match seen.len() {
0 => Err(format!("{name}: no probes")),
1 => Ok(seen.remove(0)),
_ => Err(format!(
"{name}: shape depends on the input ({}) — not advertisable as fixed",
seen.join(" vs ")
)),
}
}
#[test]
fn report_observed_shapes() {
// Run with --nocapture to regenerate the DECLARED table from evidence.
println!("--- observed shapes ---");
for (name, arg_sets) in probes() {
match agreed_shape(name, &arg_sets) {
Ok(s) => println!(" (\"{name}\", \"{s}\"),"),
Err(why) => println!(" // {why}"),
}
}
}
#[test]
fn every_declared_shape_is_proven() {
let probes = probes();
let mut wrong = Vec::new();
for (name, declared) in DECLARED {
let Some((_, arg_sets)) = probes.iter().find(|(n, _)| n == name) else {
wrong.push(format!(" {name}: declared `{declared}` but has no probe"));
continue;
};
match agreed_shape(name, arg_sets) {
Err(why) => wrong.push(format!(" declared `{declared}` but {why}")),
Ok(actual) if actual != *declared => {
wrong.push(format!(" {name}: declared `{declared}`, observed `{actual}`"))
}
Ok(_) => {}
}
}
assert!(
wrong.is_empty(),
"{} advertised shape(s) are not what the builtin returns:\n{}",
wrong.len(),
wrong.join("\n")
);
}
#[test]
fn a_probe_that_disagrees_with_itself_is_not_declared() {
// The load-bearing rule: an input-dependent shape must never reach DECLARED.
// `values` returns whatever the record held, so its two probes disagree —
// and a single probe would have "proved" whichever type the test happened
// to use. Assert the mechanism actually fires, or it is decoration.
let probes = probes();
let (_, arg_sets) = probes
.iter()
.find(|(n, _)| *n == "values")
.expect("values is probed");
let result = agreed_shape("values", arg_sets);
assert!(
result.is_err(),
"expected `values` to be detected as input-dependent, got {result:?}"
);
assert!(
!DECLARED.iter().any(|(n, _)| *n == "values"),
"an input-dependent shape must not be advertised as fixed"
);
}
#[test]
fn every_probe_is_declared_or_provably_undeclarable() {
// Stops a probe from being dropped while its claim stays standing, and stops
// a builtin from being declared without one. A probe may be absent from
// DECLARED only when it cannot agree with itself.
let mut bad = Vec::new();
for (name, arg_sets) in probes() {
let declared = DECLARED.iter().any(|(d, _)| *d == name);
match (agreed_shape(name, &arg_sets), declared) {
(Ok(s), false) => bad.push(format!(
" {name}: probes agree on `{s}` but it is never advertised"
)),
(Err(why), true) => bad.push(format!(" {name}: advertised, but {why}")),
_ => {}
}
}
assert!(
bad.is_empty(),
"{} probe(s) out of step with shapes::DECLARED:\n{}",
bad.len(),
bad.join("\n")
);
}
#[test]
fn declared_is_sorted_and_unique() {
let names: Vec<&str> = DECLARED.iter().map(|(n, _)| *n).collect();
let mut sorted = names.clone();
sorted.sort_unstable();
sorted.dedup();
assert_eq!(names, sorted, "shapes::DECLARED must be sorted and unique");
}