carlos / platform Public

Download this file

1	package engines
2
3	import (
4	"fmt"
5	"os"
6	"sort"
7	"strings"
8	"testing"
9	)
10
11	// Witness scenarios, in hostlife's shape (internal/sim/hostlife/witness_test.go).
12	//
13	// The random sweep reaches some interleavings rarely. A witness is one
14	// fixed, hand-scheduled scenario for one rule: it forces exactly the
15	// interleaving the rule exists for, as a sequence of protocol steps, and
16	// draws nothing from the world's RNG. It must hold (no invariant violated)
17	// with the rules in place, and violate its named invariant when the rule's
18	// mutation is applied, alone or in the stated combination.
19	//
20	// A witness calls w.check() at each step boundary, as doStep does in the
21	// sweep; event invariants (INV-P at delivery) are recorded inside the step.
22
23	type witness struct {
24	rule string // the rule it is for
25	needs string // the mutation set under which it must violate: the rule alone, or a combination the rule belongs to
26	want string // the failure the scenario names: a substring of the first violation; "+X" parts must also be recorded
27	note string // what it shows
28	run func(t *testing.T, w *world)
29	}
30
31	var witnesses = []witness{
32	{"set-before-repoint", "set-before-repoint", "INV-I1+INV-P",
33	"R2-1: adoption of a declaring build over a public route; between the repoint and the restart's gate a public request socket-activates the live unit under 0 (INV-I1 at the start) and is served by the declaring build (INV-P)", wSetBeforeRepoint},
34	{"set-before-repoint", "set-before-repoint", "INV-I1",
35	"R2-1: between the repoint and the restart's gate, Restart=always starts the live unit, a declaring build, under 0; the restart then fences and replaces it, so only the check at the start sees it", wSetBeforeRepointSystemd},
36	{"fence-needs-reload", "fence-needs-reload", "INV-I1",
37	"R10-1: the edge's reload keeps failing; a failed reload that advances the fenced counter lets adoption repoint and start the declaring build under the public map", wFenceNeedsReload},
38	{"fence-drains-admitted", "fence-drains-admitted", "INV-P",
39	"R3-1: a request admitted at 0 waits in the activator's queue across the adoption; a fence that does not drain it lets it resume into the declaring build", wFenceDrainsAdmitted},
40	{"fence-box-wide", "fence-box-wide", "INV-P",
41	"R13-2: a request admitted through a service row aimed at the engine's backend; the row is deleted, the request held across a declaring adoption; a fence scoped to the group's rows leaves it, and it resumes into the engine", wFenceBoxWide},
42	{"gate-adopt", "gate-adopt,set-before-repoint", "INV-I1",
43	"redundant alone: adoption's set-before is the same gate reached earlier, so with it in place the restart's gate finds the group fenced; with both gone adoption starts the declaring build under 0", wGateAdopt},
44	{"gate-swap", "gate-swap", "INV-I1",
45	"R7-1: a generation swap's incoming generation is a declaring build; ungated, it starts under 0", wGateSwap},
46	{"gate-fallback", "gate-fallback", "INV-I1+INV-P",
47	"R9-1: after --public the first wake fails and the wake plan falls back to a declaring GoodVersion; ungated, it starts under 0 (INV-I1) and the triggering public request is served by it (INV-P)", wGateFallback},
48	{"gate-recovery", "gate-recovery", "INV-I1",
49	"R9-1: wake recovery picks a declaring GoodVersion; ungated, it starts under 0", wGateRecovery},
50	{"gate-seed", "gate-seed", "INV-I1",
51	"a seed of a declaring build; ungated, it starts under 0", wGateSeed},
52	{"gate-cmd", "gate-cmd", "INV-I1",
53	"a carlos run command of a declaring build; ungated, it starts under 0", wGateCmd},
54	{"gate-waits-when-written", "gate-waits-when-written", "INV-I1",
55	"R10-1: adoption times out with 1 written and the reload failing; a gate that waits only when it wrote the mark lets wake recovery start a declaring GoodVersion under the public map", wGateWaitsWhenWritten},
56	{"unreadable-declares", "unreadable-declares", "INV-I1",
57	"a declaring build whose manifest cannot be read, launched under 0; read as non-declaring, it starts under 0", wUnreadableDeclares},
58	{"live-link-only-adoption", "live-link-only-adoption", "INV-I1",
59	"R11: something other than adoption moves the live link to a declaring build; systemd's Restart=always starts it, ungated, under 0", wLiveLinkOnly},
60	{"mark-on-final-upstream", "mark-on-final-upstream", "INV-P",
61	"R1-2: a public request through an alias whose final upstream is the engine; checked on the alias row, it reaches the engine", wMarkOnFinalUpstreamAlias},
62	{"mark-on-final-upstream", "mark-on-final-upstream", "INV-P",
63	"R1-2: a public request through a static row's path map whose final upstream is the engine; checked on the static row, it reaches the engine", wMarkOnFinalUpstreamPath},
64
65	// Task 3: classification, minted groups, the operator clear
66	{"classify-null-refused", "classify-null-refused", "INV-P",
67	"R2-2: the engine runs a declaring build whose live manifest cannot be read; the upgrade leaves it NULL; an edge that serves NULL like 0 admits a public request into the engine", wClassifyNullRefused},
68	{"classify-staged", "classify-staged", "INV-I1+INV-P",
69	"R8-1: an awake engine is repointed to a plain build without a restart, so the declaring build still runs; an upgrade that reads only the live manifest classifies the group 0, under the running engine (INV-I1) and a public request reaches it (INV-P)", wClassifyStaged},
70	{"classify-staged", "classify-staged,dedicated-launch-check", "INV-I1",
71	"R8-1, app scope: two instances of one app; the declaring build is staged once, by the other instance; this one runs it from that copy, is repointed to a plain build without a restart and upgraded; read per group, or without the staged clause, it classifies 0 under the running engine. Since Task 4 the launch check refuses the second instance's declaring adoption (another group's row on the box), so it needs that check gone too, and the edge's dedicated refusal keeps the public out (INV-I1 only)", wClassifyStagedApp},
72	{"minted-follow-owner", "minted-follow-owner,dedicated-launch-check,dedicated-edge-refusal", "INV-P",
73	"R5-1: an app minted a platform row while public; adoption of a declaring build marks and fences the app; a minted row that is its own group stays 0 and a public request by the minted host reaches the engine", wMintedFollowOwner},
74	{"minted-follow-owner", "minted-follow-owner", "INV-P",
75	"R5-1, by the grant: --grant doc-engine on the minted row of a public app; a minted row that is its own group takes the mark alone, and a public request by the app's own host reaches the granted app", wMintedFollowOwnerGrant},
76	{"grant-marks-group", "grant-marks-group", "INV-P",
77	"R6-1: --grant doc-engine on the minted row of a plain release; a grant that marks only when it is on the owner's own row leaves the group 0, and a public request by the minted host reaches the granted app", wGrantMarksGroup},
78	{"static-minted-public", "static-minted-public", "INV-AV",
79	"R6-2: a static app with a minted row and a canary; an upgrade that classifies minted static rows like instance rows leaves them NULL, and they never answer (liveness)", wStaticMintedPublic},
80	{"owner-nonempty-unique", "owner-nonempty-unique,dedicated-edge-refusal", "INV-P",
81	"R7-2: an engine instance's minted row was minted before owners were recorded; a fallback that matches empty sockets puts it in the group of a later plain instance of the app, so --public on that instance writes 0 on the engine's minted row. Since Task 4 its availability effect is gone (a misgrouped row on a box that homes a closed group is refused by design either way) and its safety effect needs the edge's dedicated refusal gone too: a public request by the minted host reaches the engine", wOwnerNonEmptyUnique},
82	{"public-checks-live", "public-checks-live", "INV-I1+INV-P",
83	"--public on a group whose live release declares; without step 1 the clear writes 0, and systemd's socket activation starts the declaring live build ungated (INV-I1) for a public request (INV-P)", wPublicChecksLive},
84	{"public-stops-group", "public-stops-group,public-confirms-empty", "INV-I1+INV-P",
85	"R7-1/R8-2: redundant alone: without the stop, step 3 finds the declaring generation still serving and refuses; with both gone, a clear after a rollout that repointed the live link to a plain build and only scheduled the swap writes 0 under the still-serving declaring generation", wPublicStopsGroup},
86	{"public-confirms-empty", "public-confirms-empty", "INV-I1+INV-P",
87	"the clear's stop does not complete and leaves the declaring generation running; without step 3 the clear writes 0 under it (INV-I1) and a public request reaches it (INV-P)", wPublicConfirmsEmpty},
88	{"public-holds-lock", "public-holds-lock", "INV-I1+INV-P",
89	"--public checks a plain live release; without the adoption lock, adoption repoints to a declaring build before the stop; the clear writes 0 over a declaring live link, and socket activation starts it ungated", wPublicHoldsLock},
90
91	// Task 4: the dedicated engine box and ingress
92	{"ports-excluded", "ports-excluded", "INV-P",
93	"R11-1: the engine route holds a port grant from a plain release, so the box renders its listener; adoption of a declaring build marks the group; a box that keeps the listener lets a public connection to the port, which the firewall admits as granted, reach the engine past the edge, with no capability pass in between", wPortsExcluded},
94	{"ports-excluded", "ports-excluded", "INV-P",
95	"R11-1, by the grant: the public engine route on a plain build holds a port grant and its listener; --grant doc-engine marks the group; a box that keeps the listener lets a public connection reach the granted group past the edge, with no capability pass in between", wPortsExcludedGrant},
96	{"dedicated-launch-check", "dedicated-launch-check,dedicated-edge-refusal", "INV-P",
97	"R12-2: redundant alone: a service row aimed at the engine's backend exists before a declaring adoption; the launch check refuses the adoption; without it the edge's refusal still refuses the row once the group is internal; with both gone a public request through the row reaches the engine", wDedicatedLaunchCheck},
98	{"dedicated-edge-refusal", "dedicated-edge-refusal", "INV-P",
99	"R12-2: a service row aimed at the engine's backend is added after the engine runs internal, where no launch check sees it; an edge that serves it lets a public request reach the engine", wDedicatedEdgeRefusal},
100	{"ingress-precondition", "ingress-precondition", "INV-P",
101	"R13-1: a service row on the calling box aimed at the engine box's address; a firewall that admits it lets a public request through the calling box's edge reach the engine directly", wIngressPrivate},
102	{"ingress-precondition", "ingress-precondition", "INV-P",
103	"R12-1: the engine binds a port of its own on every interface; a firewall that admits it lets a public connection reach the engine", wOwnPort},
104
105	// Task 5: calls, identity, grants and arming
106	{"cgroup-identity", "cgroup-identity", "INV-ID",
107	"R1-1: on an armed box a sibling instance's process connects to the granted instance's engine socket (mode 0666); a socket whose path is the identity records the granted app as the caller", wCgroupIdentity},
108	{"door-uid", "door-uid", "INV-ID",
109	"R2-3: a flat tenant running as carlos reads a granted app's door key and calls an engine through the door; a door that takes the key from uid carlos records the granted app as the caller", wDoorUID},
110	{"hop-caller-signed", "hop-caller-signed", "INV-ID",
111	"a public client sends the engine box a request carrying X-Carlos-Hop-Caller naming a granted app; an engine box that takes the caller from the header rather than a verified hop records that app as the caller", wHopCallerSigned},
112	{"engine-box-recheck", "engine-box-recheck", "INV-G",
113	"G4: a revoke is read everywhere; the calling box is rebuilt (no floor) and a bucket writer at once replays the record the revoke superseded, still inside its ten minutes; the calling box admits on it; an engine box that trusts the calling box's admission serves the revoked app although it has read the revoke", wEngineBoxRecheck},
114	{"exact-route-engine", "exact-route-engine", "INV-G",
115	"R4-2: an app holds engine A's grant only; A's hostname is a static row whose path map points at engine B's route; an engine call resolved through the path map reaches B", wExactRouteEngine},
116	{"floor-persisted", "floor-persisted", "INV-G",
117	"R1-4: a grant is revoked and read everywhere; a bucket writer at once replays the older record, still inside its ten minutes, which the floor refuses; both edges restart; a floor not persisted admits the replay, and the revoke both boxes had read is no longer in force", wFloorPersisted},
118	{"stale-clears-grants", "stale-clears-grants,grant-freshness-bound", "INV-G",
119	"§6.4: redundant alone: a table's record was signed no later than its last good read, so the signed_at bound empties a stale table first. The bucket is unreachable when a revoke is published; ten minutes pass with no good read; with both checks gone the stale table still grants and serves the revoked app", wStaleClearsGrants},
120	{"armed-refuses-unisolated", "armed-refuses-unisolated", "INV-ARM",
121	"R3-2/R4-1: on an armed box with engine sockets open, a foreign instance starts and a worker spawns; a box that does not refuse them runs unisolated tenant code beside open sockets", wArmedRefusesUnisolated},
122	{"armed-refuses-unisolated", "armed-refuses-unisolated", "INV-ARM",
123	"R4-1: on an armed box, an app's worker spawns into carlos-exec@ (worker alone)", wArmedRefusesWorker},
124	{"armed-refuses-unisolated", "armed-refuses-unisolated", "INV-ARM",
125	"R3-2: on an armed box, a flat instance starts (flat alone)", wArmedRefusesFlat},
126	{"arm-checks-box", "arm-checks-box", "INV-ARM",
127	"R5-2: an app's worker runs in carlos-exec@ on an unarmed box; arming that does not check the box opens engine sockets beside it", wArmChecksBox},
128
129	// Final review
130	{"new-group-fenced", "new-group-fenced", "INV-I1+INV-P",
131	"a public request is admitted through a service row aimed at address X and held; the row is deleted; a declaring instance is provisioned at X; a new row's NULL taken as fenced lets its first launch skip the reload, so the held request is never drained and reaches the engine", wNewGroupFenced},
132	{"grant-freshness-bound", "grant-freshness-bound", "INV-G",
133	"R5: the console re-signs (revision 2) and both edges read it; it revokes shop (revision 3) and a bucket writer puts revision 2 back before any edge reads 3; the floor admits it (equal revision); a mirror with no signed_at bound keeps the revoked grant until revision 2 expires, so a call ten minutes and one poll later reaches the engine", wGrantFreshnessBound},
134	{"clear-launch-lock", "clear-launch-lock", "INV-I1+INV-P",
135	"--public on an internal group whose live release is plain; after its empty check and before its write of 0, a carlos run command of a declaring build passes the gate (the group is still fenced as internal); a launch that ignores the group's lock starts it, and --public writes 0 under it", wClearLaunchLock},
136	}
137
138	// TestWitnesses is the deterministic half of the mutation evidence.
139	//
140	// With no mutation (the gate) it proves every witness's claim in full: the
141	// scenario holds with every rule in place, holds under every proper subset of
142	// its stated mutation set (so a rule a combination names is shown necessary,
143	// not assumed), and under the whole set violates the failure the scenario
144	// names, not merely some invariant.
145	//
146	// Under ENGINESIM_MUTATE=m (the harness) it runs the witnesses of the rules
147	// in m; a witness whose set is within m must violate with its named failure.
148	// ENGINESIM_WITNESS=rule runs one rule's witnesses with their trace.
149	func TestWitnesses(t *testing.T) {
150	only := os.Getenv("ENGINESIM_WITNESS")
151	if mutated == "" {
152	ran := 0
153	for _, x := range witnesses {
154	if only != "" && x.rule != only {
155	continue
156	}
157	ran++
158	check(t, x, "", false, only != "")
159	for _, s := range properSubsets(x.needs) {
160	check(t, x, s, false, only != "")
161	}
162	check(t, x, x.needs, true, only != "")
163	}
164	if only != "" && ran == 0 {
165	t.Fatalf("no witness for rule %q", only)
166	}
167	return
168	}
169	set := mutationSet(mutated)
170	for _, x := range witnesses {
171	if only != "" && x.rule != only {
172	continue
173	}
174	if !set[x.rule] {
175	continue
176	}
177	needs := true
178	for _, m := range strings.Split(x.needs, ",") {
179	if !set[m] {
180	needs = false
181	}
182	}
183	if needs {
184	check(t, x, mutated, true, only != "")
185	continue
186	}
187	// the mutation set is not the witness's: report, enforce nothing
188	report(t, x, mutated, only != "")
189	}
190	}
191
192	// TestWitnessRulesKnown: every witness names a rule in allRules, and so does
193	// every member of its mutation set.
194	func TestWitnessRulesKnown(t *testing.T) {
195	known := map[string]bool{}
196	for _, r := range allRules {
197	known[r] = true
198	}
199	for _, x := range witnesses {
200	if !known[x.rule] {
201	t.Errorf("witness for unknown rule %q", x.rule)
202	}
203	for _, m := range strings.Split(x.needs, ",") {
204	if !known[m] {
205	t.Errorf("witness %s needs unknown rule %q", x.rule, m)
206	}
207	}
208	}
209	}
210
211	func report(t *testing.T, x witness, m string, trace bool) {
212	saved := mutated
213	mutated = m
214	defer func() { mutated = saved }()
215	w := newWitness()
216	x.run(t, w)
217	tag := "held"
218	if len(w.violations) > 0 {
219	tag = "violated: " + w.violations[0]
220	}
221	t.Logf("witness %s under %q (needs %q): %s", x.rule, m, x.needs, tag)
222	if trace {
223	dump(t, w)
224	}
225	}
226
227	// check runs one witness under mutation m, reports it, and fails the test if
228	// the outcome is not the stated one: held when no violation is expected, the
229	// named failure when one is.
230	func check(t *testing.T, x witness, m string, expectViolation bool, trace bool) {
231	saved := mutated
232	mutated = m
233	defer func() { mutated = saved }()
234	w := newWitness()
235	x.run(t, w)
236	violated := len(w.violations) > 0
237	tag := "held"
238	if violated {
239	tag = "violated: " + w.violations[0]
240	}
241	t.Logf("witness %s under %q (needs %q): %s", x.rule, m, x.needs, tag)
242	switch {
243	case expectViolation && !violated:
244	t.Errorf("witness %s held under %q, which it must violate", x.rule, m)
245	dump(t, w)
246	case expectViolation && !wantMet(w.violations, x.want):
247	t.Errorf("witness %s under %q violated, but not its named failure %q", x.rule, m, x.want)
248	dump(t, w)
249	case !expectViolation && violated:
250	t.Errorf("witness %s violated under %q, where it must hold", x.rule, m)
251	dump(t, w)
252	}
253	if trace {
254	dump(t, w)
255	}
256	}
257
258	// wantMet: the first violation names want's first part, and every further
259	// "+" part is named by some recorded violation.
260	func wantMet(vs []string, want string) bool {
261	parts := strings.Split(want, "+")
262	if len(vs) == 0 || !namedFailure(vs[0], parts[0]) {
263	return false
264	}
265	for _, f := range parts[1:] {
266	found := false
267	for _, v := range vs {
268	found = found || namedFailure(v, f)
269	}
270	if !found {
271	return false
272	}
273	}
274	return true
275	}
276
277	// namedFailure: the violation names the witness's failure. want is one
278	// failure or several separated by "|"; a failure that ends in a digit must not
279	// run on into another (INV-I1 is not INV-I10).
280	func namedFailure(v, want string) bool {
281	for _, f := range strings.Split(want, "|") {
282	for i := 0; ; {
283	j := strings.Index(v[i:], f)
284	if j < 0 {
285	break
286	}
287	end := i + j + len(f)
288	last := f[len(f)-1]
289	if !(last >= '0' && last <= '9') || end == len(v) || v[end] < '0' || v[end] > '9' {
290	return true
291	}
292	i = i + j + 1
293	}
294	}
295	return false
296	}
297
298	func mutationSet(m string) map[string]bool {
299	set := map[string]bool{}
300	for _, x := range strings.Split(m, ",") {
301	if x != "" {
302	set[x] = true
303	}
304	}
305	return set
306	}
307
308	// properSubsets: every non-empty proper subset of a comma-separated set.
309	func properSubsets(needs string) []string {
310	xs := strings.Split(needs, ",")
311	var out []string
312	for mask := 1; mask < (1<<len(xs))-1; mask++ {
313	var sub []string
314	for i, x := range xs {
315	if mask&(1<<i) != 0 {
316	sub = append(sub, x)
317	}
318	}
319	out = append(out, strings.Join(sub, ","))
320	}
321	return out
322	}
323
324	func dump(t *testing.T, w *world) {
325	for _, line := range w.trace {
326	t.Log(line)
327	}
328	t.Logf("state: %s", w.boxesState())
329	}
330
331	// boxesState is a one-line summary of every box, for a failing witness.
332	func (w *world) boxesState() string {
333	var out []string
334	for _, b := range w.boxes {
335	hosts := make([]string, 0, len(b.Rows))
336	for h := range b.Rows {
337	hosts = append(hosts, h)
338	}
339	sort.Strings(hosts)
340	var marks []string
341	for _, h := range hosts {
342	marks = append(marks, fmt.Sprintf("%s=%v/%v", h, b.Mark[h], b.Serving[h]))
343	}
344	var procs []string
345	for _, p := range b.Procs {
346	procs = append(procs, fmt.Sprintf("%d:%s@v%d", p.ID, p.Group, p.Ver))
347	}
348	var adm []string
349	for _, r := range b.Admitted {
350	adm = append(adm, fmt.Sprintf("%d:%s@e%d", r.ID, r.Row, r.Epoch))
351	}
352	out = append(out, fmt.Sprintf("box%d{marks(reg/edge) %v wrote=%d fenced=%d epoch=%d reloadFails=%v live=%v good=%v procs=%v admitted=%v}",
353	b.ID, marks, b.Wrote, b.Fenced, b.Epoch, b.ReloadFails, b.Live, b.Good, procs, adm))
354	}
355	return strings.Join(out, " ")
356	}
357
358	// ---------- the fixture ----------
359
360	// The witness builds: one of each kind, fixed, so no scenario depends on a
361	// seed's draw.
362	const (
363	vPlain = 1 // reads, does not declare
364	vEngine = 2 // reads, declares doc_engine
365	vUnreadable = 3 // declares, but its manifest cannot be read
366	vBlind = 4 // does not declare, manifest unreadable
367	)
368
369	func newWitness() *world {
370	w := newWorld(0, true)
371	w.builds = map[int]build{
372	vPlain: {Ver: vPlain, Declares: false, ManifestOK: true},
373	vEngine: {Ver: vEngine, Declares: true, ManifestOK: true},
374	vUnreadable: {Ver: vUnreadable, Declares: true, ManifestOK: false},
375	vBlind: {Ver: vBlind, Declares: false, ManifestOK: false},
376	}
377	w.logf("witness world: builds %s", w.buildsString())
378	return w
379	}
380
381	// clearPublic is the operator's --public on group g (operatorPublic), then
382	// the edge's next poll, as one witness step. False when the clear refused.
383	func (w *world) clearPublic(b *box, g string) bool {
384	ok := w.operatorPublic(b, g)
385	w.reload(b)
386	w.check()
387	return ok
388	}
389
390	// publicEngine sets the engine group on box 0 to a public route serving the
391	// plain build: live and good are vPlain, the mark is 0 and fenced, and one
392	// process runs.
393	func (w *world) publicEngine(t *testing.T) *box {
394	b := w.boxes[0]
395	b.Live[eng], b.Good[eng] = vPlain, vPlain
396	if !w.clearPublic(b, eng) {
397	t.Fatalf("witness: --public refused on a plain live release: %s", w.boxesState())
398	}
399	if !w.launch(b, eng, vPlain, "seed") {
400	t.Fatalf("witness: the plain build did not start under 0: %s", w.boxesState())
401	}
402	w.check()
403	if len(w.violations) > 0 {
404	t.Fatalf("witness: the fixture violates: %v", w.violations)
405	}
406	return b
407	}
408
409	// ---------- the witnesses ----------
410
411	// wSetBeforeRepoint (R2-1): adoption repoints the live link to a declaring
412	// build; before its restart a public request arrives, socket activation
413	// starts the live unit (no activator, no gate) and serves it. With the mark
414	// set and fenced before the repoint, the request is refused.
415	func wSetBeforeRepoint(t *testing.T, w *world) {
416	b := w.publicEngine(t)
417	w.stopGroup(b, eng)
418	w.adopt(b, eng, vEngine, func() {
419	if r := w.admitPublic(b, engHost, "/"); r != nil {
420	w.socketActivate(b, eng)
421	w.deliver(r)
422	}
423	})
424	w.check()
425	}
426
427	// wSetBeforeRepointSystemd (R2-1): adoption repoints the live link to a
428	// declaring build; before its restart, Restart=always starts the live unit
429	// (no activator, no gate). No request is involved.
430	func wSetBeforeRepointSystemd(t *testing.T, w *world) {
431	b := w.publicEngine(t)
432	w.adopt(b, eng, vEngine, func() { w.systemdRestart(b, eng) })
433	w.check()
434	}
435
436	// wFenceDrainsAdmitted (R3-1): a request admitted at 0 waits in the
437	// activator's queue while adoption marks, fences, repoints and restarts; it
438	// then resumes.
439	func wFenceDrainsAdmitted(t *testing.T, w *world) {
440	b := w.publicEngine(t)
441	r := w.admitPublic(b, engHost, "/")
442	if r == nil {
443	t.Fatalf("witness: a public request to a public route was refused")
444	}
445	r.Held = true
446	w.adopt(b, eng, vEngine, nil)
447	w.check()
448	w.deliver(r)
449	w.check()
450	}
451
452	// r10Sequence (R10-1): the edge's reload fails; adoption of a declaring
453	// build writes 1 and times out without repointing; then wake recovery picks
454	// the declaring GoodVersion.
455	func r10Sequence(t *testing.T, w *world) {
456	b := w.publicEngine(t)
457	b.Good[eng] = vEngine
458	b.ReloadFails = true
459	w.logf("witness: the edge's reload starts failing")
460	w.adopt(b, eng, vEngine, nil)
461	w.check()
462	w.stopGroup(b, eng)
463	w.wake(b, eng, "recovery", nil)
464	w.check()
465	}
466
467	func wFenceNeedsReload(t *testing.T, w *world) { r10Sequence(t, w) }
468	func wGateWaitsWhenWritten(t *testing.T, w *world) { r10Sequence(t, w) }
469
470	// wFenceBoxWide (R13-2): a service row aimed at the engine's backend admits a
471	// public request; the row is deleted and the request held; adoption of a
472	// declaring build fences the group; the request resumes on the proxy it
473	// already holds.
474	func wFenceBoxWide(t *testing.T, w *world) {
475	b := w.publicEngine(t)
476	const svc = "svc.example"
477	b.Rows[svc] = &row{Host: svc, Kind: "service", Backend: b.Rows[engHost].Backend, PathTo: map[string]string{}}
478	b.Mark[svc] = markPublic
479	w.reload(b)
480	w.check()
481	r := w.admitPublic(b, svc, "/")
482	if r == nil {
483	t.Fatalf("witness: the service row refused a public request: %s", w.boxesState())
484	}
485	r.Held = true
486	delete(b.Rows, svc)
487	delete(b.Mark, svc)
488	w.logf("witness: row %s deleted; request %d still holds its proxy", svc, r.ID)
489	w.adopt(b, eng, vEngine, nil)
490	w.check()
491	w.deliver(r)
492	w.check()
493	}
494
495	// wGateAdopt: adoption of a declaring build with no other start.
496	func wGateAdopt(t *testing.T, w *world) {
497	b := w.publicEngine(t)
498	w.adopt(b, eng, vEngine, nil)
499	w.check()
500	}
501
502	// wGateSwap (R7-1), wGateSeed, wGateCmd, wGateRecovery: a declaring build
503	// started by that path under 0.
504	func gatePath(path string) func(*testing.T, *world) {
505	return func(t *testing.T, w *world) {
506	b := w.publicEngine(t)
507	if path == "recovery" {
508	b.Good[eng] = vEngine
509	w.stopGroup(b, eng)
510	w.wake(b, eng, "recovery", nil)
511	} else {
512	w.launch(b, eng, vEngine, path)
513	}
514	w.check()
515	}
516	}
517
518	func wGateSwap(t *testing.T, w *world) { gatePath("swap")(t, w) }
519	func wGateSeed(t *testing.T, w *world) { gatePath("seed")(t, w) }
520	func wGateCmd(t *testing.T, w *world) { gatePath("cmd")(t, w) }
521	func wGateRecovery(t *testing.T, w *world) { gatePath("recovery")(t, w) }
522
523	// oraclePublic makes box 0's engine group public on a plain live release.
524	func oraclePublic(w *world, b *box) {
525	b.Live[eng] = vPlain
526	w.clearPublic(b, eng)
527	}
528
529	// wGateFallback (R9-1): the group ran a declaring build, was adopted to a
530	// plain one (the mark stays 1) and cleared with --public; a public request
531	// wakes it, the first wake fails and the plan falls back to the declaring
532	// GoodVersion.
533	func wGateFallback(t *testing.T, w *world) {
534	b := w.boxes[0]
535	b.Live[eng], b.Good[eng] = vEngine, vEngine
536	if !w.launch(b, eng, vEngine, "seed") {
537	t.Fatalf("witness: the engine did not start under its fenced mark: %s", w.boxesState())
538	}
539	w.check()
540	w.adopt(b, eng, vPlain, nil)
541	w.check()
542	b.Good[eng] = vEngine // the plain build has not proved itself yet
543	if !w.clearPublic(b, eng) {
544	t.Fatalf("witness: --public refused on a plain live release: %s", w.boxesState())
545	}
546	r := w.admitPublic(b, engHost, "/")
547	if r == nil {
548	t.Fatalf("witness: a public request after --public was refused: %s", w.boxesState())
549	}
550	r.Held = true
551	w.wake(b, eng, "fallback", r)
552	w.check()
553	}
554
555	// wUnreadableDeclares: a build that declares but whose manifest cannot be
556	// read, seeded under 0.
557	func wUnreadableDeclares(t *testing.T, w *world) {
558	b := w.publicEngine(t)
559	w.launch(b, eng, vUnreadable, "seed")
560	w.check()
561	}
562
563	// wLiveLinkOnly (R11): something other than adoption moves the live link to
564	// a declaring build, then systemd restarts the unit from the live link.
565	func wLiveLinkOnly(t *testing.T, w *world) {
566	b := w.publicEngine(t)
567	w.moveLive(b, eng, vEngine, "a rollout tool")
568	w.check()
569	w.systemdRestart(b, eng)
570	w.check()
571	}
572
573	// markOnFinalUpstream (R1-2): the engine runs fenced as internal; one public
574	// request arrives by host and path, a row that resolves to the engine's row.
575	func markOnFinalUpstream(t *testing.T, w *world, host, path string) {
576	b := w.boxes[0]
577	b.Live[eng], b.Good[eng] = vEngine, vEngine
578	if !w.launch(b, eng, vEngine, "seed") {
579	t.Fatalf("witness: the engine did not start under its fenced mark: %s", w.boxesState())
580	}
581	w.check()
582	if r := w.admitPublic(b, host, path); r != nil {
583	w.deliver(r)
584	}
585	w.check()
586	}
587
588	func wMarkOnFinalUpstreamAlias(t *testing.T, w *world) { markOnFinalUpstream(t, w, engAlias, "/") }
589	func wMarkOnFinalUpstreamPath(t *testing.T, w *world) {
590	markOnFinalUpstream(t, w, engSite, engSitePath)
591	}
592
593	// ---------- Task 3: classification, minted groups, the operator clear ----------
594
595	// requestBy sends one public request by host and delivers it if admitted.
596	func (w *world) requestBy(b *box, host string) {
597	if r := w.admitPublic(b, host, "/"); r != nil {
598	w.deliver(r)
599	}
600	}
601
602	// wClassifyNullRefused (R2-2): the engine's live release declares but its
603	// manifest cannot be read; the upgrade can classify it neither way, so it
604	// stays NULL; a public request arrives.
605	func wClassifyNullRefused(t *testing.T, w *world) {
606	b := w.boxes[0]
607	if !w.adopt(b, eng, vUnreadable, nil) {
608	t.Fatalf("witness: adoption of the engine refused: %s", w.boxesState())
609	}
610	w.check()
611	w.upgrade(b)
612	w.check()
613	if m := w.groupMark(b, eng); m != markNull {
614	t.Fatalf("witness: the upgrade classified an unreadable live release %v, want NULL", m)
615	}
616	w.requestBy(b, engHost)
617	w.check()
618	}
619
620	// wClassifyStaged (R8-1): the engine runs a declaring build; adoption of a
621	// plain build repoints the awake route without a restart, so the declaring
622	// build keeps running; then the agent upgrades and a public request arrives.
623	func wClassifyStaged(t *testing.T, w *world) {
624	b := w.boxes[0]
625	if !w.adopt(b, eng, vEngine, nil) {
626	t.Fatalf("witness: adoption of the engine refused: %s", w.boxesState())
627	}
628	w.check()
629	if !w.repointAwake(b, eng, vPlain) {
630	t.Fatalf("witness: the awake repoint was refused: %s", w.boxesState())
631	}
632	w.check()
633	w.upgrade(b)
634	w.check()
635	w.requestBy(b, engHost)
636	w.check()
637	}
638
639	// wClassifyStagedApp (R8-1, app scope): tcp-a stages the declaring build
640	// first; tcp-b, another instance of the app, adopts the same build (staged
641	// for the app already, so recorded under tcp-a only), is repointed to a
642	// plain build without a restart, and the agent upgrades.
643	//
644	// Since Task 4 the launch check refuses tcp-b's declaring adoption beside
645	// tcp-a (a proxying row of another group): the model has no era before the
646	// upgrade in which launches pass no gate, so this scenario needs the launch
647	// check gone too. The edge's dedicated refusal then still refuses tcp-b's
648	// public request (tcp-a is homed internal), so it violates INV-I1 only.
649	func wClassifyStagedApp(t *testing.T, w *world) {
650	b := w.engineFreeBox(t)
651	if !w.provision(b, tcpA, tcpApp, "10.0.0.7:9101", vEngine) || !w.provision(b, tcpB, tcpApp, "10.0.0.7:9102", vPlain) {
652	t.Fatalf("witness: provisioning refused: %s", w.boxesState())
653	}
654	if !w.adopt(b, tcpB, vEngine, nil) {
655	if on("dedicated-launch-check") {
656	w.logf("witness: the launch check refuses %s's declaring adoption beside %s; on a dedicated box the scenario cannot arise", tcpB, tcpA)
657	return
658	}
659	t.Fatalf("witness: adoption of the declaring build refused: %s", w.boxesState())
660	}
661	w.check()
662	for _, v := range b.Staged[tcpB] {
663	if v == vEngine {
664	t.Fatalf("witness: the declaring build is recorded under %s too; the scenario needs it staged for the other instance only", tcpB)
665	}
666	}
667	if !w.repointAwake(b, tcpB, vPlain) {
668	t.Fatalf("witness: the awake repoint was refused: %s", w.boxesState())
669	}
670	w.check()
671	w.upgrade(b)
672	w.check()
673	w.requestBy(b, tcpB)
674	w.check()
675	}
676
677	const (
678	tcpApp = "acct/tcp"
679	tcpA = "tcp-a"
680	tcpB = "tcp-b"
681	tcpC = "tcp-c"
682	tcpD = "tcp-d"
683	mintedB = "tcp-b.acct.apps.example"
684	mintedC = "tcp-c.acct.apps.example"
685	)
686
687	// tcpPublic provisions a TCP-backed instance tcp-b of a plain build and mints
688	// its platform row with the owner recorded; both answer publicly.
689	func (w *world) tcpPublic(t *testing.T, b *box) {
690	if !w.provision(b, tcpB, tcpApp, "10.0.0.7:9102", vPlain) {
691	t.Fatalf("witness: provisioning %s refused: %s", tcpB, w.boxesState())
692	}
693	w.mint(b, tcpB, mintedB, true)
694	w.reload(b)
695	w.check()
696	if r := w.admitPublic(b, mintedB, "/"); r == nil {
697	t.Fatalf("witness: the minted row of a public app refused a public request: %s", w.boxesState())
698	} else {
699	w.deliver(r)
700	}
701	w.check()
702	if len(w.violations) > 0 {
703	t.Fatalf("witness: the fixture violates: %v", w.violations)
704	}
705	}
706
707	// wMintedFollowOwner (R5-1): a public app with a minted row adopts a
708	// declaring build; a public request arrives by the minted host.
709	//
710	// Since Task 4 a minted row that is its own group is a proxying row of
711	// another group: the launch check refuses the adoption beside it, and the
712	// edge's dedicated refusal refuses it once the app is internal. The witness
713	// needs both gone with minted-follow-owner.
714	func wMintedFollowOwner(t *testing.T, w *world) {
715	b := w.engineFreeBox(t)
716	w.tcpPublic(t, b)
717	if !w.adopt(b, tcpB, vEngine, nil) {
718	if on("minted-follow-owner") || !on("dedicated-launch-check") {
719	t.Fatalf("witness: adoption of the declaring build refused: %s", w.boxesState())
720	}
721	w.logf("witness: the minted row, its own group, is another group's row beside %s; the launch check refuses the adoption", tcpB)
722	return
723	}
724	w.check()
725	w.requestBy(b, mintedB)
726	w.check()
727	}
728
729	// wMintedFollowOwnerGrant (R5-1, by the grant): a public app of a plain
730	// build with a minted row; the operator grants doc-engine on the minted row;
731	// a public request arrives by the app's own host.
732	func wMintedFollowOwnerGrant(t *testing.T, w *world) {
733	b := w.engineFreeBox(t)
734	w.tcpPublic(t, b)
735	w.grant(b, mintedB)
736	w.check()
737	w.requestBy(b, tcpB)
738	w.check()
739	}
740
741	// wGrantMarksGroup (R6-1): a public app of a plain build with a minted row;
742	// the operator grants doc-engine on the minted row; a public request arrives
743	// by the minted host.
744	func wGrantMarksGroup(t *testing.T, w *world) {
745	b := w.engineFreeBox(t)
746	w.tcpPublic(t, b)
747	w.grant(b, mintedB)
748	w.check()
749	w.requestBy(b, mintedB)
750	w.check()
751	}
752
753	// wStaticMintedPublic (R6-2): a static app with its minted row and a canary
754	// on its own channel; the agent upgrades; at the end every public row must
755	// answer.
756	func wStaticMintedPublic(t *testing.T, w *world) {
757	b := w.boxes[0]
758	w.addStaticApp(b, "site")
759	w.reload(b)
760	w.check()
761	w.upgrade(b)
762	w.check()
763	w.final()
764	}
765
766	// wOwnerNonEmptyUnique (R7-2): app acct/tcp's TCP instance tcp-b runs a
767	// declaring build, internal; its platform row was minted before owners were
768	// recorded, so the edge finds its owner by backend. tcp-a, a later plain
769	// instance of the app, is cleared with --public. A public request arrives by
770	// tcp-b's minted host.
771	//
772	// Task 3's version ended in INV-AV: tcp-b's public minted row, misgrouped
773	// into a closed group, never answered. Since Task 4 a closed group homes its
774	// box, so every row outside it, the misgrouped row included (its true group
775	// is tcp-b), is refused by design and INV-AV does not count it. The safety
776	// effect remains, behind the edge's dedicated refusal.
777	func wOwnerNonEmptyUnique(t *testing.T, w *world) {
778	b := w.engineFreeBox(t)
779	if !w.provision(b, tcpB, tcpApp, "10.0.0.7:9102", vEngine) {
780	t.Fatalf("witness: provisioning %s refused: %s", tcpB, w.boxesState())
781	}
782	w.mint(b, tcpB, mintedB, false)
783	w.reload(b)
784	w.check()
785	if !w.provision(b, tcpA, tcpApp, "10.0.0.7:9101", vPlain) {
786	t.Fatalf("witness: provisioning %s refused: %s", tcpA, w.boxesState())
787	}
788	w.check()
789	if !w.clearPublic(b, tcpA) {
790	t.Fatalf("witness: --public refused on %s's plain live release: %s", tcpA, w.boxesState())
791	}
792	w.requestBy(b, mintedB)
793	w.check()
794	}
795
796	// wPublicChecksLive: the engine's live release declares; the operator runs
797	// --public; a public request arrives and socket activation starts the unit.
798	func wPublicChecksLive(t *testing.T, w *world) {
799	b := w.boxes[0]
800	if !w.adopt(b, eng, vEngine, nil) {
801	t.Fatalf("witness: adoption of the engine refused: %s", w.boxesState())
802	}
803	w.check()
804	w.clearPublic(b, eng)
805	r := w.admitPublic(b, engHost, "/")
806	w.socketActivate(b, eng)
807	if r != nil {
808	w.deliver(r)
809	}
810	w.check()
811	}
812
813	// wPublicStopsGroup (R7-1, R8-2): the engine runs a declaring generation; a
814	// generation rollout of a plain build repoints the live link and only
815	// schedules the swap; the operator runs --public; a public request arrives.
816	func wPublicStopsGroup(t *testing.T, w *world) {
817	b := w.boxes[0]
818	if !w.adopt(b, eng, vEngine, nil) {
819	t.Fatalf("witness: adoption of the engine refused: %s", w.boxesState())
820	}
821	w.check()
822	if !w.repointAwake(b, eng, vPlain) {
823	t.Fatalf("witness: the rollout's repoint was refused: %s", w.boxesState())
824	}
825	w.check()
826	w.clearPublic(b, eng)
827	w.requestBy(b, engHost)
828	w.check()
829	}
830
831	// wPublicConfirmsEmpty: the engine runs a declaring generation; a rollout of
832	// a plain build repoints the live link and only schedules the swap; the
833	// operator runs --public and its stop leaves that generation running; a
834	// public request arrives.
835	func wPublicConfirmsEmpty(t *testing.T, w *world) {
836	b := w.boxes[0]
837	if !w.adopt(b, eng, vEngine, nil) {
838	t.Fatalf("witness: adoption of the engine refused: %s", w.boxesState())
839	}
840	w.check()
841	if !w.repointAwake(b, eng, vPlain) {
842	t.Fatalf("witness: the rollout's repoint was refused: %s", w.boxesState())
843	}
844	w.check()
845	w.clearStopMisses = true
846	w.clearPublic(b, eng)
847	w.clearStopMisses = false
848	w.requestBy(b, engHost)
849	w.check()
850	}
851
852	// TestGrantRefusedOnUnresolvedMintedRow: --grant doc-engine on a minted row
853	// whose owner is not recorded and cannot be found uniquely (here two
854	// instances of its app share its address) is refused; the row stays NULL at
855	// the edge and refused, and no group is marked.
856	func TestGrantRefusedOnUnresolvedMintedRow(t *testing.T) {
857	w := newWitness()
858	b := w.engineFreeBox(t)
859	for _, h := range []string{tcpC, tcpD} {
860	if !w.provision(b, h, tcpApp, "10.0.0.7:9103", vPlain) {
861	t.Fatalf("provisioning %s refused: %s", h, w.boxesState())
862	}
863	}
864	w.mint(b, tcpC, mintedC, false)
865	// and one whose recorded owner has no row
866	b.Rows["gone"] = &row{Host: "gone", Kind: "instance", App: tcpApp, Backend: "10.0.0.7:9104", PathTo: map[string]string{}}
867	w.mint(b, "gone", "gone.acct.apps.example", true)
868	delete(b.Rows, "gone")
869	w.reload(b)
870	wrote := b.Wrote
871	for _, h := range []string{mintedC, "gone.acct.apps.example"} {
872	if w.grant(b, h) {
873	t.Errorf("--grant on %s, whose owner cannot be resolved, succeeded", h)
874	}
875	if b.Rows[h].Grant {
876	t.Errorf("--grant on %s recorded the grant", h)
877	}
878	if b.Serving[h] != markNull {
879	t.Errorf("the edge serves %s %v, want NULL", h, b.Serving[h])
880	}
881	if r := w.admitPublic(b, h, "/"); r != nil {
882	t.Errorf("a public request to %s was admitted", h)
883	}
884	}
885	if b.Wrote != wrote {
886	t.Errorf("a refused grant changed the registry (%d to %d)", wrote, b.Wrote)
887	}
888	for _, g := range []string{tcpC, tcpD} {
889	if m := w.groupMark(b, g); m != markPublic {
890	t.Errorf("group %s is %v after a refused grant, want public", g, m)
891	}
892	}
893	if len(w.violations) > 0 {
894	t.Errorf("violations: %v", w.violations)
895	}
896	if t.Failed() {
897	dump(t, w)
898	}
899	}
900
901	// TestRevokeRunsTheBarrier: --grant on a minted row times out while the
902	// edge's reload fails (1 written, not fenced); a public request is admitted
903	// and held; --revoke through the minted row also times out and the mark stays
904	// 1; adoption of a declaring build is refused for want of the fence. Once
905	// the reload recovers, the fence drains the held request, the declaring
906	// build starts, and nothing public reaches it. With the reload working,
907	// --revoke returns once the edge has loaded it, and the mark is still 1.
908	func TestRevokeRunsTheBarrier(t *testing.T) {
909	w := newWitness()
910	b := w.engineFreeBox(t)
911	w.tcpPublic(t, b)
912	b.ReloadFails = true
913	if w.grant(b, mintedB) {
914	t.Fatal("--grant returned loaded while the edge's reload fails")
915	}
916	if m := w.groupMark(b, tcpB); m != markInternal {
917	t.Fatalf("after the timed-out grant the group is %v, want internal", m)
918	}
919	held := w.admitPublic(b, tcpB, "/")
920	if held == nil {
921	t.Fatalf("the edge (still serving 0) refused a public request: %s", w.boxesState())
922	}
923	held.Held = true
924	if w.revoke(b, mintedB) {
925	t.Fatal("--revoke returned loaded while the edge's reload fails")
926	}
927	if b.Rows[mintedB].Grant {
928	t.Fatal("--revoke left the grant recorded")
929	}
930	if m := w.groupMark(b, tcpB); m != markInternal {
931	t.Fatalf("--revoke changed the mark to %v; only --public writes 0", m)
932	}
933	if w.adopt(b, tcpB, vEngine, nil) {
934	t.Fatalf("adoption of a declaring build passed the gate without a fence: %s", w.boxesState())
935	}
936	w.check()
937	b.ReloadFails = false
938	if !w.adopt(b, tcpB, vEngine, nil) {
939	t.Fatalf("adoption refused after the reload recovered: %s", w.boxesState())
940	}
941	w.check()
942	w.deliver(held)
943	if held.Reached != 0 {
944	t.Fatalf("the request admitted before the fence reached process %d", held.Reached)
945	}
946	for _, h := range []string{tcpB, mintedB} {
947	if r := w.admitPublic(b, h, "/"); r != nil {
948	t.Fatalf("a public request to %s was admitted after the fence", h)
949	}
950	}
951	// with the reload working, revoke waits for the edge and returns loaded
952	w.grant(b, tcpB)
953	if !w.revoke(b, tcpB) || b.Fenced < b.Wrote {
954	t.Fatalf("--revoke with a working reload did not return loaded: %s", w.boxesState())
955	}
956	if m := w.groupMark(b, tcpB); m != markInternal || !w.fenced(b, tcpB) {
957	t.Fatalf("after --revoke the group is %v (fenced %v), want internal and fenced", m, w.fenced(b, tcpB))
958	}
959	if len(w.violations) > 0 {
960	t.Fatalf("violations: %v", w.violations)
961	}
962	if t.Failed() {
963	dump(t, w)
964	}
965	}
966
967	// wPublicHoldsLock: the engine was adopted to a plain build (the mark stays
968	// 1); the operator runs --public; after its checks pass and before it stops
969	// the group, adoption of a declaring build runs; then a public request
970	// arrives and socket activation starts the unit.
971	func wPublicHoldsLock(t *testing.T, w *world) {
972	b := w.boxes[0]
973	if !w.adopt(b, eng, vEngine, nil) || !w.adopt(b, eng, vPlain, nil) {
974	t.Fatalf("witness: adoption refused: %s", w.boxesState())
975	}
976	w.check()
977	w.clearHook = func(hb *box, g, stage string) {
978	if stage == "locked" {
979	w.adopt(hb, g, vEngine, nil)
980	}
981	}
982	w.clearPublic(b, eng)
983	w.clearHook = nil
984	r := w.admitPublic(b, engHost, "/")
985	w.socketActivate(b, eng)
986	if r != nil {
987	w.deliver(r)
988	}
989	w.check()
990	}
991
992	// TestI1Oracle pins INV-I1 on hand-built states of box 0's engine group with
993	// a declaring process running: the fence condition alone catches a group that
994	// is NULL, unloaded by the edge, or written and swapped but unacknowledged;
995	// the served-map condition alone catches a counter advanced without a swap.
996	// A NULL group counts as closed once the edge has fenced the change that made
997	// it NULL: the edge refuses NULL like 1 (spec §5.1 "The column"), and the
998	// upgrade leaves a group NULL under a running declaring build whose live
999	// manifest cannot be read (Task 3). A new row's NULL, which no change closed
1000	// and no reload has drained, never counts (final review, finding 1).
1001	func TestI1Oracle(t *testing.T) {
1002	cases := []struct {
1003	name string
1004	setup func(w *world, b *box)
1005	want string // "" holds; else a substring of the reason
1006	}{
1007	{"fenced as internal", func(w *world, b *box) {}, ""},
1008	{"NULL written over 0, not yet fenced", func(w *world, b *box) {
1009	oraclePublic(w, b)
1010	w.writeMark(b, eng, markNull)
1011	}, "not fenced"},
1012	{"NULL written over 0 and fenced (the edge treats NULL like 1)", func(w *world, b *box) {
1013	oraclePublic(w, b)
1014	w.writeMark(b, eng, markNull)
1015	w.reload(b)
1016	}, ""},
1017	{"a new row, NULL, with no fence generation", func(w *world, b *box) {
1018	for _, h := range []string{eng, engHost} {
1019	delete(b.Rows, h)
1020	delete(b.Mark, h)
1021	}
1022	delete(b.SetAt, eng)
1023	b.Rows[eng] = &row{Host: eng, Kind: "instance", App: "acct/eng", Backend: "/run/carlos/eng.sock", PathTo: map[string]string{}}
1024	b.Wrote++
1025	w.reload(b)
1026	}, "not fenced"},
1027	{"NULL on one row, 0 served on the other", func(w *world, b *box) {
1028	oraclePublic(w, b)
1029	b.Mark[engHost] = markNull
1030	b.Serving[engHost] = markNull
1031	}, "not fenced"},
1032	{"written 1, absent from the edge's map", func(w *world, b *box) {
1033	oraclePublic(w, b)
1034	w.writeMark(b, eng, markInternal)
1035	delete(b.EdgeRows, engHost)
1036	delete(b.Serving, engHost)
1037	}, "not fenced"},
1038	{"written 1 and swapped in, fence not acknowledged", func(w *world, b *box) {
1039	oraclePublic(w, b)
1040	w.writeMark(b, eng, markInternal)
1041	b.Serving[engHost] = markInternal
1042	}, "not fenced"},
1043	{"counter advanced without a swap", func(w *world, b *box) {
1044	oraclePublic(w, b)
1045	w.writeMark(b, eng, markInternal)
1046	b.Fenced = b.Wrote
1047	}, "serves " + eng + " public"},
1048	}
1049	for _, c := range cases {
1050	w := newWitness()
1051	b := w.boxes[0]
1052	c.setup(w, b)
1053	p := &proc{ID: 99, Group: eng, Ver: vEngine, Slice: "inst:" + eng}
1054	b.Procs = append(b.Procs, p)
1055	why := w.i1Broken(b, p)
1056	w.check()
1057	switch {
1058	case c.want == "" && (why != "" || len(w.violations) > 0):
1059	t.Errorf("%s: want held, got %q %v", c.name, why, w.violations)
1060	case c.want != "" && !strings.Contains(why, c.want):
1061	t.Errorf("%s: reason %q, want it to name %q", c.name, why, c.want)
1062	case c.want != "" && (len(w.violations) != 1 || invariantOf(w.violations[0]) != "INV-I1"):
1063	t.Errorf("%s: check recorded %v, want one INV-I1", c.name, w.violations)
1064	}
1065	// a plain build in the same state breaks nothing
1066	p.Ver = vPlain
1067	if why := w.i1Broken(b, p); why != "" {
1068	t.Errorf("%s: a non-declaring process breaks I1: %q", c.name, why)
1069	}
1070	}
1071	}
1072
1073	// ---------- Task 4: the dedicated engine box and ingress ----------
1074
1075	const (
1076	svcHost = "svc.example" // a service row of the witnesses
1077	tcpE = "tcp-e" // a TCP-backed engine on box 0
1078	tcpEAddr = "10.0.0.7:9200"
1079	)
1080
1081	// engineFreeBox is box 0 with the engine's rows removed, the edge reloaded:
1082	// a box that homes no internal group, for scenarios that need instances of
1083	// their own (the dedicated-box rule refuses every other proxying row on a box
1084	// that homes the engine, and refuses a declaring launch beside one).
1085	func (w *world) engineFreeBox(t *testing.T) *box {
1086	b := w.boxes[0]
1087	for _, h := range []string{eng, engHost, engAlias, engSite} {
1088	delete(b.Rows, h)
1089	delete(b.Mark, h)
1090	}
1091	delete(b.SetAt, eng)
1092	b.Wrote++
1093	w.logf("witness: box0's engine rows removed (registry change %d)", b.Wrote)
1094	w.reload(b)
1095	w.check()
1096	if len(w.violations) > 0 {
1097	t.Fatalf("witness: the fixture violates: %v", w.violations)
1098	}
1099	return b
1100	}
1101
1102	// runningEngine starts the engine group on box 0 on the declaring build,
1103	// fenced as internal (its starting mark), and returns its process.
1104	func (w *world) runningEngine(t *testing.T) (*box, *proc) {
1105	b := w.boxes[0]
1106	b.Live[eng], b.Good[eng] = vEngine, vEngine
1107	if !w.launch(b, eng, vEngine, "seed") {
1108	t.Fatalf("witness: the engine did not start under its fenced mark: %s", w.boxesState())
1109	}
1110	w.check()
1111	if len(w.violations) > 0 {
1112	t.Fatalf("witness: the fixture violates: %v", w.violations)
1113	}
1114	return b, b.Procs[len(b.Procs)-1]
1115	}
1116
1117	// portsEngine is the public engine route shipping a plain release declaring
1118	// ports: the box renders its listener, and a public connection to the port
1119	// reaches the plain build. It returns the port.
1120	func (w *world) portsEngine(t *testing.T) (*box, string) {
1121	b := w.publicEngine(t)
1122	if !w.ship(b, eng, vPlain, true) {
1123	t.Fatalf("witness: a plain release declaring ports was refused: %s", w.boxesState())
1124	}
1125	port := b.PortGrant[eng]
1126	if port == "" || b.Listen[port] != eng {
1127	t.Fatalf("witness: no listener rendered for the granted port: %s", w.boxesState())
1128	}
1129	if p := w.directConnect(b, port, true); p == nil {
1130	t.Fatalf("witness: the granted port of a public route reached nothing: %s", w.boxesState())
1131	}
1132	w.check()
1133	return b, port
1134	}
1135
1136	// listenerGone fails the witness if the write that closed the group left
1137	// port's listener in place, while ports-excluded holds: the write removes it
1138	// itself, before any fence and with no capability pass (final review, minor
1139	// 2).
1140	func (w *world) listenerGone(t *testing.T, b *box, port, after string) {
1141	if on("ports-excluded") && b.Listen[port] != "" {
1142	t.Fatalf("witness: the listener on %s is still there right after %s: %s", port, after, w.boxesState())
1143	}
1144	}
1145
1146	// wPortsExcluded (R11-1): the public engine route ships a plain release
1147	// declaring ports, and the box renders its listener; then adoption of a
1148	// declaring build; at once, with no capability pass, a public connection
1149	// arrives on the granted port.
1150	func wPortsExcluded(t *testing.T, w *world) {
1151	b, port := w.portsEngine(t)
1152	if !w.adopt(b, eng, vEngine, nil) {
1153	t.Fatalf("witness: adoption of the engine refused: %s", w.boxesState())
1154	}
1155	w.listenerGone(t, b, port, "the adoption")
1156	w.check()
1157	w.directConnect(b, port, true)
1158	w.check()
1159	}
1160
1161	// wPortsExcludedGrant (R11-1, by the grant): the public engine route serves a
1162	// plain build on its ports listener; the operator grants doc-engine on it; at
1163	// once, with no capability pass, a public connection arrives on the port.
1164	func wPortsExcludedGrant(t *testing.T, w *world) {
1165	b, port := w.portsEngine(t)
1166	w.grant(b, engHost)
1167	w.listenerGone(t, b, port, "the grant")
1168	w.check()
1169	w.directConnect(b, port, true)
1170	w.check()
1171	}
1172
1173	// TestPortsListenerGoneOnNull (final review, minor 2): the upgrade leaves a
1174	// route with no live release NULL; the write of NULL removes its ports
1175	// listener at once, before the capability pass runs, and a public connection
1176	// to the port is refused by the firewall.
1177	func TestPortsListenerGoneOnNull(t *testing.T) {
1178	w := newWitness()
1179	b := w.boxes[1]
1180	b.PortGrant["shop"] = "40001"
1181	w.capsPass(b)
1182	if b.Listen["40001"] != "shop" {
1183	t.Fatalf("fixture: no listener for shop's grant: %s", w.boxesState())
1184	}
1185	w.upgrade(b)
1186	if m := w.groupMark(b, "shop"); m != markNull {
1187	t.Fatalf("fixture: shop is %v after the upgrade, want NULL", m)
1188	}
1189	if b.Listen["40001"] != "" {
1190	t.Errorf("the listener is still there right after the upgrade's NULL: %s", w.boxesState())
1191	}
1192	if p := w.directConnect(b, "40001", true); p != nil {
1193	t.Errorf("a public connection to the NULL route's port reached process %d", p.ID)
1194	}
1195	w.check()
1196	if len(w.violations) > 0 {
1197	t.Errorf("violations: %v", w.violations)
1198	}
1199	if t.Failed() {
1200	dump(t, w)
1201	}
1202	}
1203
1204	// wDedicatedLaunchCheck (R12-2): the public engine route has a service row
1205	// beside it aimed at its backend; adoption of a declaring build; a public
1206	// request arrives through the service row.
1207	func wDedicatedLaunchCheck(t *testing.T, w *world) {
1208	b := w.publicEngine(t)
1209	w.addServiceRow(b, svcHost, b.Rows[eng].Backend)
1210	w.reload(b)
1211	w.check()
1212	ok := w.adopt(b, eng, vEngine, nil)
1213	if ok && on("dedicated-launch-check") {
1214	t.Fatalf("witness: a declaring adoption passed the launch check beside a service row: %s", w.boxesState())
1215	}
1216	w.check()
1217	w.requestBy(b, svcHost)
1218	w.check()
1219	}
1220
1221	// wDedicatedEdgeRefusal (R12-2): the engine runs internal; a service row
1222	// aimed at its backend is added afterwards; the edge polls; a public request
1223	// arrives through the service row.
1224	func wDedicatedEdgeRefusal(t *testing.T, w *world) {
1225	b, _ := w.runningEngine(t)
1226	w.addServiceRow(b, svcHost, b.Rows[eng].Backend)
1227	w.reload(b)
1228	w.check()
1229	w.requestBy(b, svcHost)
1230	w.check()
1231	}
1232
1233	// wIngressPrivate (R13-1): a TCP-backed engine runs internal on box 0; a
1234	// service row on box 1 is aimed at box 0's address and the engine's port; a
1235	// public request arrives at box 1's edge through it.
1236	func wIngressPrivate(t *testing.T, w *world) {
1237	b0, b1 := w.engineFreeBox(t), w.boxes[1]
1238	if !w.provision(b0, tcpE, tcpApp, tcpEAddr, vEngine) {
1239	t.Fatalf("witness: provisioning the TCP engine refused: %s", w.boxesState())
1240	}
1241	w.check()
1242	w.addServiceRow(b1, svcHost, tcpEAddr)
1243	w.reload(b1)
1244	w.check()
1245	r := w.admitPublic(b1, svcHost, "/")
1246	if r == nil {
1247	t.Fatalf("witness: box1's edge refused its own service row: %s", w.boxesState())
1248	}
1249	w.deliver(r)
1250	w.check()
1251	}
1252
1253	// wOwnPort (R12-1): the engine runs internal and binds a port of its own on
1254	// every interface; a public connection arrives on that port.
1255	func wOwnPort(t *testing.T, w *world) {
1256	b, p := w.runningEngine(t)
1257	w.bindOwnPort(b, p)
1258	w.directConnect(b, ownPort(p), true)
1259	w.check()
1260	}
1261
1262	// TestNullRouteHomesTheBox: a NULL route homes its box like a route marked
1263	// 1, whether or not it has a release. Here box 1's shop has no release, so
1264	// the upgrade leaves it NULL; a service row aimed at its backend must get the
1265	// internal refusal. Were it served, a request admitted through it and held,
1266	// with the row then deleted, would outlive a declaring `carlos run` in the
1267	// NULL group: the gate writes 1 over NULL, a group already fenced, so no
1268	// reload bumps the epoch, and the launch check finds no row to refuse.
1269	func TestNullRouteHomesTheBox(t *testing.T) {
1270	w := newWitness()
1271	b := w.boxes[1]
1272	w.upgrade(b)
1273	if m := w.groupMark(b, "shop"); m != markNull || b.Live["shop"] != 0 {
1274	t.Fatalf("fixture: shop is %v with live v%d, want NULL with no release", m, b.Live["shop"])
1275	}
1276	w.addServiceRow(b, svcHost, b.Rows["shop"].Backend)
1277	w.reload(b)
1278	r := w.admitPublic(b, svcHost, "/")
1279	if r != nil {
1280	r.Held = true
1281	w.deleteRow(b, svcHost)
1282	w.launch(b, "shop", vEngine, "cmd")
1283	w.deliver(r)
1284	}
1285	w.check()
1286	if r != nil {
1287	t.Errorf("a service row beside a NULL route was served (request %d)", r.ID)
1288	}
1289	if len(w.violations) > 0 {
1290	t.Errorf("violations: %v", w.violations)
1291	}
1292	if t.Failed() {
1293	dump(t, w)
1294	}
1295	}
1296
1297	// TestShipRefusesDocEngineWithPorts (spec §8): `carlos ship` refuses a
1298	// release declaring doc_engine and ports together, and nothing is adopted or
1299	// granted; a plain release declaring ports ships, and its port listens.
1300	func TestShipRefusesDocEngineWithPorts(t *testing.T) {
1301	w := newWitness()
1302	b := w.publicEngine(t)
1303	wrote := b.Wrote
1304	if w.ship(b, eng, vEngine, true) {
1305	t.Fatal("a release declaring doc_engine and ports shipped")
1306	}
1307	if b.Live[eng] != vPlain || b.PortGrant[eng] != "" || len(b.Listen) != 0 || b.Wrote != wrote {
1308	t.Fatalf("a refused ship changed the box: %s", w.boxesState())
1309	}
1310	if !w.ship(b, eng, vPlain, true) || b.Listen[b.PortGrant[eng]] != eng {
1311	t.Fatalf("a plain release declaring ports did not ship with its listener: %s", w.boxesState())
1312	}
1313	if len(w.violations) > 0 {
1314	t.Fatalf("violations: %v", w.violations)
1315	}
1316	}
1317
1318	// TestEngineBoxKeepsStaticRows (spec §8): on a box homing an internal group,
1319	// a service row aimed at the engine and another app's instance get the
1320	// internal refusal, a declaring launch beside them is refused, and the
1321	// static row keeps answering.
1322	func TestEngineBoxKeepsStaticRows(t *testing.T) {
1323	w := newWitness()
1324	b, _ := w.runningEngine(t)
1325	w.addServiceRow(b, svcHost, b.Rows[eng].Backend)
1326	b.Rows["other"] = &row{Host: "other", Kind: "instance", App: "acct/other", Backend: "10.0.0.7:9300", PathTo: map[string]string{}}
1327	b.Mark["other"] = markPublic
1328	w.reload(b)
1329	for _, h := range []string{svcHost, "other"} {
1330	if _, outcome := w.admit(b, h, "/"); outcome != refused {
1331	t.Errorf("%s on the engine's box: %s, want the internal refusal", h, outcome)
1332	}
1333	}
1334	if _, outcome := w.admit(b, engSite, "/"); outcome != answered {
1335	t.Errorf("the static row %s on the engine's box: %s, want answered", engSite, outcome)
1336	}
1337	if w.launch(b, eng, vEngine, "seed") {
1338	t.Errorf("a declaring launch beside other proxying rows was not refused")
1339	}
1340	w.check()
1341	if len(w.violations) > 0 {
1342	t.Errorf("violations: %v", w.violations)
1343	}
1344	if t.Failed() {
1345	dump(t, w)
1346	}
1347	}
1348
1349	// wNewGroupFenced (final review, finding 1): on a box that homes nothing, a
1350	// service row aimed at address X admits a public request, which is held; the
1351	// row is deleted; a declaring instance is provisioned at X. Its row is new
1352	// and NULL, but the edge has never loaded it: its first launch must write 1
1353	// and wait for a fence, whose epoch bump drains the held request.
1354	func wNewGroupFenced(t *testing.T, w *world) {
1355	b := w.engineFreeBox(t)
1356	w.addServiceRow(b, svcHost, tcpEAddr)
1357	w.reload(b)
1358	w.check()
1359	r := w.admitPublic(b, svcHost, "/")
1360	if r == nil {
1361	t.Fatalf("witness: the service row refused a public request: %s", w.boxesState())
1362	}
1363	r.Held = true
1364	w.deleteRow(b, svcHost)
1365	if !w.provision(b, tcpE, tcpApp, tcpEAddr, vEngine) {
1366	t.Fatalf("witness: provisioning the declaring instance refused: %s", w.boxesState())
1367	}
1368	w.check()
1369	w.deliver(r)
1370	w.check()
1371	}
1372
1373	// wClearLaunchLock (final review, finding 2): the engine was adopted to a
1374	// plain build (the mark stays 1); the operator runs --public; after its empty
1375	// check, a carlos run command of the declaring build tries to start; then a
1376	// public request arrives.
1377	func wClearLaunchLock(t *testing.T, w *world) {
1378	b := w.boxes[0]
1379	if !w.adopt(b, eng, vEngine, nil) || !w.adopt(b, eng, vPlain, nil) {
1380	t.Fatalf("witness: adoption refused: %s", w.boxesState())
1381	}
1382	w.check()
1383	w.clearHook = func(hb *box, g, stage string) {
1384	if stage == "confirmed" {
1385	w.launch(hb, g, vEngine, "cmd")
1386	}
1387	}
1388	w.clearPublic(b, eng)
1389	w.clearHook = nil
1390	w.requestBy(b, engHost)
1391	w.check()
1392	}
1393
1394	// wGrantFreshnessBound (final review, finding 3; ruling R5): thirty ticks in,
1395	// the console re-signs (revision 2, granting shop) and both edges read it;
1396	// the console revokes shop (revision 3) and a bucket writer puts revision 2
1397	// back before any edge reads 3. Each edge reads revision 2 again (equal to
1398	// its floor: the same signed bytes). Shop calls at once (within the bound),
1399	// then again ten minutes and one poll after the revoke.
1400	func wGrantFreshnessBound(t *testing.T, w *world) {
1401	w.runningEngine(t)
1402	shop := w.armedShop(t)
1403	w.advance(30)
1404	w.publish(w.console.Rev + 1) // the periodic re-sign: revision 2, signed at 30
1405	w.pollAll()
1406	w.consoleRevoke(shopEng) // revision 3, at 30
1407	w.replay(2)
1408	w.pollAll()
1409	w.check()
1410	w.engineCall(w.boxes[1], shop, false, "carlos", "shop", eng, "/")
1411	w.check()
1412	w.advance(staleTicks + pollTicks + 1)
1413	w.pollAll()
1414	w.engineCall(w.boxes[1], shop, false, "carlos", "shop", eng, "/")
1415	w.check()
1416	}
1417
1418	// TestReplayBoundedBySignedAt (ruling R5): wGrantFreshnessBound's replay, with
1419	// every rule in place, keeps the revoked grant on both edges until the
1420	// replayed record's signed_at plus ten minutes, and not one tick longer.
1421	func TestReplayBoundedBySignedAt(t *testing.T) {
1422	w := newWitness()
1423	w.runningEngine(t)
1424	shop := w.armedShop(t)
1425	w.advance(30)
1426	w.publish(w.console.Rev + 1)
1427	signed := w.now()
1428	w.pollAll()
1429	w.consoleRevoke(shopEng)
1430	w.replay(2)
1431	w.advance(staleTicks - 1) // 59 ticks after revision 2 was signed
1432	w.pollAll()
1433	if !w.engineCall(w.boxes[1], shop, false, "carlos", "shop", eng, "/") {
1434	t.Errorf("at signed_at+%d the replayed record should still grant (the bound is not tighter than R5): %s", w.now()-signed, w.mirrorsState())
1435	}
1436	w.advance(1)
1437	w.pollAll()
1438	if w.engineCall(w.boxes[1], shop, false, "carlos", "shop", eng, "/") {
1439	t.Errorf("at signed_at+%d the replayed record still grants: %s", w.now()-signed, w.mirrorsState())
1440	}
1441	w.check()
1442	if len(w.violations) > 0 || len(w.residuals) > 0 {
1443	t.Errorf("violations %v residuals %v", w.violations, w.residuals)
1444	}
1445	if t.Failed() {
1446	dump(t, w)
1447	}
1448	}
1449
1450	// ---------- Task 5: calls, identity, grants and arming ----------
1451
1452	// shopEng is the grant every Task 5 world starts with: shop may call eng.
1453	const shopEng = "acct/shop/eng"
1454
1455	// armedShop starts shop on box 1 on the plain build and arms box 1, so
1456	// shop's engine socket is open. It returns shop's process.
1457	func (w *world) armedShop(t *testing.T) *proc {
1458	b := w.boxes[1]
1459	b.Live["shop"], b.Good["shop"] = vPlain, vPlain
1460	if !w.launch(b, "shop", vPlain, "seed") {
1461	t.Fatalf("witness: shop did not start: %s", w.boxesState())
1462	}
1463	if !w.arm(b) {
1464	t.Fatalf("witness: arming box 1 with only nested shop refused: %s", w.boxesState())
1465	}
1466	w.check()
1467	if len(w.violations) > 0 {
1468	t.Fatalf("witness: the fixture violates: %v", w.violations)
1469	}
1470	return w.newest(b, "shop")
1471	}
1472
1473	// pollAll is one mirror poll on every box.
1474	func (w *world) pollAll() {
1475	for _, b := range w.boxes {
1476	w.mirrorTick(b)
1477	}
1478	}
1479
1480	// wCgroupIdentity (R1-1): box 1 runs shop and a sibling instance, other,
1481	// and is armed; other's process connects to shop's engine socket.
1482	func wCgroupIdentity(t *testing.T, w *world) {
1483	w.runningEngine(t)
1484	b := w.boxes[1]
1485	if !w.provision(b, "other", "acct/other", "127.0.0.1:9002", vPlain) {
1486	t.Fatalf("witness: provisioning other refused: %s", w.boxesState())
1487	}
1488	w.armedShop(t)
1489	op := w.newest(b, "other")
1490	if op == nil {
1491	t.Fatalf("witness: other is not running: %s", w.boxesState())
1492	}
1493	w.engineCall(b, op, false, "carlos", "shop", eng, "/")
1494	w.check()
1495	}
1496
1497	// wDoorUID (R2-3): a flat tenant on unarmed box 1, running as carlos,
1498	// presents shop's door key with Host: eng.
1499	func wDoorUID(t *testing.T, w *world) {
1500	w.runningEngine(t)
1501	b := w.boxes[1]
1502	if !w.launchUnisolated(b, "flat") {
1503	t.Fatalf("witness: a flat start on an unarmed box refused: %s", w.boxesState())
1504	}
1505	w.check()
1506	w.engineCall(b, w.newest(b, "flat"), true, "carlos", "shop", eng, "/")
1507	w.check()
1508	}
1509
1510	// wHopCallerSigned: a public client sends box 0 a request for the engine's
1511	// hostname carrying X-Carlos-Hop-Caller: acct/shop/eng and no hop MAC.
1512	func wHopCallerSigned(t *testing.T, w *world) {
1513	b, _ := w.runningEngine(t)
1514	w.clientHop(b, engHost, "/", callerOf("acct/shop", eng))
1515	w.check()
1516	}
1517
1518	// wEngineBoxRecheck (G4): shop's grant is revoked and read everywhere; box
1519	// 1's data directory is lost (a rebuilt box: no floor), and a bucket writer
1520	// at once replays revision 1, signed moments ago; box 1 accepts it, box 0's
1521	// floor refuses it; shop calls eng.
1522	func wEngineBoxRecheck(t *testing.T, w *world) {
1523	w.runningEngine(t)
1524	shop := w.armedShop(t)
1525	b1 := w.boxes[1]
1526	w.consoleRevoke(shopEng)
1527	w.pollAll()
1528	w.rebuild(b1)
1529	w.replay(1)
1530	w.pollAll()
1531	w.check()
1532	if !w.tableGrants(b1, shopEng) {
1533	t.Fatalf("witness: the rebuilt calling box does not hold the replayed grant: %s", w.mirrorsState())
1534	}
1535	w.engineCall(b1, shop, false, "carlos", "shop", eng, "/")
1536	w.check()
1537	}
1538
1539	// wExactRouteEngine (R4-2): shop holds engine site's grant and not eng's;
1540	// site's hostname is box 0's static row, whose path map sends /convert to
1541	// eng's route; shop calls site at /convert.
1542	func wExactRouteEngine(t *testing.T, w *world) {
1543	w.runningEngine(t)
1544	shop := w.armedShop(t)
1545	w.consoleGrant("acct/shop/" + site)
1546	w.consoleRevoke(shopEng)
1547	w.pollAll()
1548	w.check()
1549	w.engineCall(w.boxes[1], shop, false, "carlos", "shop", site, engSitePath)
1550	w.check()
1551	}
1552
1553	// wFloorPersisted (R1-4): shop's grant is revoked and read everywhere; a
1554	// bucket writer at once replays revision 1 (signed moments ago), which both
1555	// floors refuse; both edges restart; each polls; shop calls eng.
1556	func wFloorPersisted(t *testing.T, w *world) {
1557	w.runningEngine(t)
1558	shop := w.armedShop(t)
1559	w.consoleRevoke(shopEng)
1560	w.pollAll()
1561	w.replay(1)
1562	w.pollAll()
1563	for _, b := range w.boxes {
1564	w.restartEdge(b)
1565	}
1566	w.pollAll()
1567	w.check()
1568	w.engineCall(w.boxes[1], shop, false, "carlos", "shop", eng, "/")
1569	w.check()
1570	}
1571
1572	// wStaleClearsGrants (§6.4): the bucket is unreachable; shop's grant is
1573	// revoked; ten minutes pass with no good read; shop calls eng.
1574	func wStaleClearsGrants(t *testing.T, w *world) {
1575	w.runningEngine(t)
1576	shop := w.armedShop(t)
1577	w.setBucketDown(true)
1578	w.consoleRevoke(shopEng)
1579	w.advance(staleTicks)
1580	w.pollAll()
1581	w.check()
1582	w.engineCall(w.boxes[1], shop, false, "carlos", "shop", eng, "/")
1583	w.check()
1584	}
1585
1586	// armedRefuses: box 1 is armed with shop's socket open; each kind of
1587	// unisolated launch is tried in turn.
1588	func armedRefuses(kinds ...string) func(*testing.T, *world) {
1589	return func(t *testing.T, w *world) {
1590	w.armedShop(t)
1591	b := w.boxes[1]
1592	for _, k := range kinds {
1593	ok := w.launchUnisolated(b, k)
1594	if ok && on("armed-refuses-unisolated") {
1595	t.Fatalf("witness: an armed box admitted a %s launch: %s", k, w.boxesState())
1596	}
1597	w.check()
1598	}
1599	}
1600	}
1601
1602	func wArmedRefusesUnisolated(t *testing.T, w *world) { armedRefuses("foreign", "worker")(t, w) }
1603	func wArmedRefusesWorker(t *testing.T, w *world) { armedRefuses("worker")(t, w) }
1604	func wArmedRefusesFlat(t *testing.T, w *world) { armedRefuses("flat")(t, w) }
1605
1606	// wArmChecksBox (R5-2): an app's worker runs in carlos-exec@ on unarmed box
1607	// 1 beside nested shop; the operator arms box 1.
1608	func wArmChecksBox(t *testing.T, w *world) {
1609	b := w.boxes[1]
1610	b.Live["shop"], b.Good["shop"] = vPlain, vPlain
1611	w.launch(b, "shop", vPlain, "seed")
1612	if !w.launchUnisolated(b, "worker") {
1613	t.Fatalf("witness: a worker spawn on an unarmed box refused: %s", w.boxesState())
1614	}
1615	w.check()
1616	ok := w.arm(b)
1617	if ok && on("arm-checks-box") {
1618	t.Fatalf("witness: arming a box with a running worker succeeded: %s", w.boxesState())
1619	}
1620	w.check()
1621	}
1622
1623	// TestResidualsAreCountedNotFailed: each of the spec's two stated residuals,
1624	// as a fixed scenario. With its flag off the scenario is a
1625	// violation (the sequence really breaks the invariant the residual
1626	// concedes); with the flag on the world records residual:<name> and no
1627	// violation. The default world never sets a flag (TestEngines asserts the
1628	// sweep records no residual).
1629	func TestResidualsAreCountedNotFailed(t *testing.T) {
1630	cases := []struct {
1631	name string
1632	set func(w *world)
1633	run func(t *testing.T, w *world)
1634	}{
1635	{"unwrittenManifestAcrossUpgrade", func(w *world) { w.unwrittenManifestAcrossUpgrade = true }, residualUnwrittenManifest},
1636	{"flatEraTamper", func(w *world) { w.flatEraTamper = true }, residualFlatEraTamper},
1637	}
1638	for _, c := range cases {
1639	t.Run(c.name, func(t *testing.T) {
1640	off := newWitness()
1641	c.run(t, off)
1642	if len(off.violations) == 0 || len(off.residuals) > 0 {
1643	t.Errorf("flag off: want a violation and no residual, got violations %v residuals %v", off.violations, off.residuals)
1644	dump(t, off)
1645	}
1646	on := newWitness()
1647	c.set(on)
1648	c.run(t, on)
1649	if len(on.violations) > 0 || len(on.residuals) == 0 {
1650	t.Errorf("flag on: want residuals and no violation, got violations %v residuals %v", on.violations, on.residuals)
1651	dump(t, on)
1652	}
1653	for _, r := range on.residuals {
1654	if !strings.HasPrefix(r, "residual:"+c.name) {
1655	t.Errorf("flag on: residual %q is not residual:%s", r, c.name)
1656	}
1657	}
1658	})
1659	}
1660	}
1661
1662	// residualUnwrittenManifest (§5.1 "Classification before serving"): the
1663	// engine runs a declaring build whose staged manifest was never written;
1664	// an awake repoint moves its live link to a plain build without a restart;
1665	// the box takes the upgrade, which classifies the group 0 under the
1666	// running engine; a public request arrives.
1667	func residualUnwrittenManifest(t *testing.T, w *world) {
1668	b := w.boxes[0]
1669	b.Live[eng], b.Good[eng] = vUnreadable, vUnreadable
1670	if !w.launch(b, eng, vUnreadable, "seed") {
1671	t.Fatalf("scenario: the engine did not start: %s", w.boxesState())
1672	}
1673	if !w.repointAwake(b, eng, vPlain) {
1674	t.Fatalf("scenario: the awake repoint refused: %s", w.boxesState())
1675	}
1676	w.check()
1677	if w.residualAtUpgrade(b) == "" {
1678	t.Fatalf("scenario: the upgrade residual is not set up: %s", w.boxesState())
1679	}
1680	w.upgrade(b)
1681	w.check()
1682	w.requestBy(b, engHost)
1683	w.check()
1684	}
1685
1686	// residualFlatEraTamper (§6.2): a flat tenant on unarmed box 1 plants code
1687	// in shop's instance directory; the operator moves the flat route off and
1688	// arms the box (arming vouches for the present, not the past); shop's next
1689	// start runs the planted code in shop's slice, which calls eng.
1690	func residualFlatEraTamper(t *testing.T, w *world) {
1691	w.runningEngine(t)
1692	b := w.boxes[1]
1693	b.Live["shop"], b.Good["shop"] = vPlain, vPlain
1694	if !w.launchUnisolated(b, "flat") {
1695	t.Fatalf("scenario: a flat start on an unarmed box refused: %s", w.boxesState())
1696	}
1697	w.tamper(b, w.newest(b, "flat"), "shop")
1698	w.moveToNested(b, "flat")
1699	if !w.arm(b) {
1700	t.Fatalf("scenario: arming refused after the flat route moved: %s", w.boxesState())
1701	}
1702	if !w.launch(b, "shop", vPlain, "seed") {
1703	t.Fatalf("scenario: shop did not start: %s", w.boxesState())
1704	}
1705	w.check()
1706	w.engineCall(b, w.newest(b, "shop"), false, "carlos", "shop", eng, "/")
1707	w.check()
1708	}
1709
1710	// TestGrantedCallsReach is the positive control for the Task 5 witnesses,
1711	// which hold by refusing: with every rule on, a granted caller reaches the
1712	// engine through the socket (across a hop) and through the door from an
1713	// enrolled host-app uid (spec §8), and a revoke is in force once read.
1714	func TestGrantedCallsReach(t *testing.T) {
1715	w := newWitness()
1716	w.runningEngine(t)
1717	shop := w.armedShop(t)
1718	b1 := w.boxes[1]
1719	if !w.engineCall(b1, shop, false, "carlos", "shop", eng, "/") {
1720	t.Errorf("shop's own process through shop's socket did not reach eng")
1721	}
1722	user := &proc{Group: "shop", Slice: "user:u-shop"}
1723	if !w.engineCall(b1, user, true, "u-shop", "shop", eng, "/") {
1724	t.Errorf("the door from shop's enrolled uid with shop's key did not reach eng")
1725	}
1726	if w.engineCall(b1, user, true, "carlos", "shop", eng, "/") {
1727	t.Errorf("the same key from uid carlos reached eng")
1728	}
1729	w.consoleRevoke(shopEng)
1730	w.pollAll()
1731	if w.engineCall(b1, shop, false, "carlos", "shop", eng, "/") {
1732	t.Errorf("a revoke read by both boxes did not stop the call")
1733	}
1734	w.check()
1735	if len(w.violations) > 0 {
1736	t.Errorf("violations: %v", w.violations)
1737	}
1738	if t.Failed() {
1739	dump(t, w)
1740	}
1741	}
1742
1743	// TestArmRefusesAndAdmits (spec §8): arming refuses a box with a flat
1744	// route, a foreign route, a route with workers, or a non-empty carlos-exec@
1745	// cgroup; it succeeds on the engine's box (a unit-backed engine) and on a box
1746	// of nested callers; on an armed box every unisolated launch is refused
1747	// before a process starts; disarm closes the engine sockets, and then
1748	// launches resume.
1749	func TestArmRefusesAndAdmits(t *testing.T) {
1750	for _, kind := range unisolatedKinds {
1751	w := newWitness()
1752	b := w.boxes[1]
1753	w.launchUnisolated(b, kind)
1754	if w.arm(b) {
1755	t.Errorf("%s: arming succeeded with the %s tenant running", kind, kind)
1756	}
1757	w.stopGroup(b, kind) // the cgroup is empty; the route remains
1758	if w.arm(b) {
1759	t.Errorf("%s: arming succeeded with a %s route on the box", kind, kind)
1760	}
1761	w.moveToNested(b, kind)
1762	if !w.arm(b) {
1763	t.Errorf("%s: arming refused once the route moved to nested", kind)
1764	}
1765	}
1766	w := newWitness()
1767	w.runningEngine(t)
1768	if !w.arm(w.boxes[0]) {
1769	t.Errorf("arming the engine's box (unit-backed engine) refused")
1770	}
1771	w.armedShop(t)
1772	b := w.boxes[1]
1773	n := len(b.Procs)
1774	for _, kind := range unisolatedKinds {
1775	if w.launchUnisolated(b, kind) {
1776	t.Errorf("an armed box admitted a %s launch", kind)
1777	}
1778	}
1779	if len(b.Procs) != n {
1780	t.Errorf("a refused launch started a process: %d -> %d", n, len(b.Procs))
1781	}
1782	w.disarm(b)
1783	if b.Sockets || b.Armed {
1784	t.Errorf("disarm left sockets %v armed %v", b.Sockets, b.Armed)
1785	}
1786	if !w.launchUnisolated(b, "worker") {
1787	t.Errorf("a worker spawn after disarm refused")
1788	}
1789	w.check()
1790	if len(w.violations) > 0 {
1791	t.Errorf("violations: %v", w.violations)
1792	}
1793	if t.Failed() {
1794	dump(t, w)
1795	}
1796	}
1797
1798	// withMutation runs f with the mutation set m, restoring the previous set.
1799	func withMutation(m string, f func()) {
1800	saved := mutated
1801	mutated = m
1802	defer func() { mutated = saved }()
1803	f()
1804	}
1805
1806	// TestExpiryKeepsRevokeAge: the grant oracle keeps expiry, staleness and
1807	// revoke age apart (final review, finding 4). With the table's own checks off
1808	// (stale-clears-grants and grant-freshness-bound), the edges keep serving a
1809	// cached grant, and the oracle alone decides:
1810	// - a key revoked long before the newest record expires is a violation by
1811	// its revoke's age, whatever the expiry;
1812	// - a key the newest record grants is a violation the moment that record
1813	// expires: an expired record admits nothing, with no grace;
1814	// - a key nobody revoked is a violation once the admitting box has had no
1815	// good read for ten minutes, whatever the revoke's age (there is none),
1816	// and not a tick earlier.
1817	func TestExpiryKeepsRevokeAge(t *testing.T) {
1818	withMutation("stale-clears-grants,grant-freshness-bound", func() {
1819	w := newWitness()
1820	w.runningEngine(t)
1821	shop := w.armedShop(t)
1822	w.setBucketDown(true)
1823	w.consoleRevoke(shopEng) // tick 0; revision 2, never read
1824	w.advance(lifetimeTicks) // revision 2 expires now
1825	w.engineCall(w.boxes[1], shop, false, "carlos", "shop", eng, "/")
1826	if len(w.violations) != 1 || invariantOf(w.violations[0]) != "INV-G" || !strings.Contains(w.violations[0], "since tick 0") {
1827	t.Errorf("a key revoked at tick 0, called across the record's expiry: want INV-G since tick 0, got %v", w.violations)
1828	dump(t, w)
1829	}
1830
1831	w = newWitness()
1832	w.runningEngine(t)
1833	shop = w.armedShop(t)
1834	w.setBucketDown(true)
1835	w.advance(lifetimeTicks) // revision 1, which grants shop, expires now
1836	w.engineCall(w.boxes[1], shop, false, "carlos", "shop", eng, "/")
1837	if len(w.violations) != 1 || invariantOf(w.violations[0]) != "INV-G" || !strings.Contains(w.violations[0], "expired at 25920") {
1838	t.Errorf("a granted key at its record's expiry: want INV-G at once, naming the expiry, got %v", w.violations)
1839	dump(t, w)
1840	}
1841
1842	w = newWitness()
1843	w.runningEngine(t)
1844	shop = w.armedShop(t)
1845	w.setBucketDown(true)
1846	w.advance(staleTicks - 1) // no good read for 59 ticks; shop still granted
1847	w.engineCall(w.boxes[1], shop, false, "carlos", "shop", eng, "/")
1848	if len(w.violations) != 0 {
1849	t.Errorf("a granted key 59 ticks after the last good read is within the bound: got %v", w.violations)
1850	dump(t, w)
1851	}
1852	w.advance(1)
1853	w.engineCall(w.boxes[1], shop, false, "carlos", "shop", eng, "/")
1854	if len(w.violations) != 1 || invariantOf(w.violations[0]) != "INV-G" || !strings.Contains(w.violations[0], "no good read") {
1855	t.Errorf("a granted key ten minutes after the last good read: want INV-G for the stale read, got %v", w.violations)
1856	dump(t, w)
1857	}
1858	})
1859	}
1860
1861	// upgradeResidualFixture is residualUnwrittenManifest up to the upgrade,
1862	// with the flag on: the residual is recorded and nothing violates. It
1863	// returns the engine's box and the tagged process.
1864	func upgradeResidualFixture(t *testing.T) (*world, *box, *proc) {
1865	w := newWitness()
1866	w.unwrittenManifestAcrossUpgrade = true
1867	b := w.boxes[0]
1868	b.Live[eng], b.Good[eng] = vUnreadable, vUnreadable
1869	w.launch(b, eng, vUnreadable, "seed")
1870	p := w.newest(b, eng)
1871	w.repointAwake(b, eng, vPlain)
1872	w.upgrade(b)
1873	w.check()
1874	if len(w.residuals) == 0 || len(w.violations) > 0 || p.Residual == "" {
1875	t.Fatalf("fixture: want the upgrade residual recorded on process %d, got residuals %v violations %v", p.ID, w.residuals, w.violations)
1876	}
1877	return w, b, p
1878	}
1879
1880	// TestResidualCoversOnlyItsOwnBreaches: a process tagged with the
1881	// unwritten-manifest residual is not a licence. While its group is still
1882	// open, a breach by a path the upgrade's 0 did not open (a public connection
1883	// to a port the engine bound itself, through a broken firewall) is a
1884	// violation. Once the group is closed again the window has ended: a later 0
1885	// written by a broken --public, under that same process, is a violation.
1886	func TestResidualCoversOnlyItsOwnBreaches(t *testing.T) {
1887	t.Run("another path", func(t *testing.T) {
1888	w, b, p := upgradeResidualFixture(t)
1889	withMutation("ingress-precondition", func() {
1890	w.bindOwnPort(b, p)
1891	w.directConnect(b, ownPort(p), true)
1892	})
1893	w.check()
1894	if len(w.violations) != 1 || invariantOf(w.violations[0]) != "INV-P" {
1895	t.Errorf("want INV-P through the broken firewall, got violations %v residuals %v", w.violations, w.residuals)
1896	dump(t, w)
1897	}
1898	})
1899	t.Run("after the window", func(t *testing.T) {
1900	w, b, p := upgradeResidualFixture(t)
1901	w.writeMark(b, eng, markInternal) // a gate's 1: the group is closed again
1902	w.reload(b)
1903	w.check()
1904	if p.Residual != "" || len(w.violations) > 0 {
1905	t.Fatalf("closing the group: want the window ended and no violation, got tag %q violations %v", p.Residual, w.violations)
1906	}
1907	withMutation("public-confirms-empty", func() {
1908	w.clearStopMisses = true
1909	w.operatorPublic(b, eng) // the stop misses process p; step 3 is gone
1910	w.reload(b)
1911	w.check()
1912	})
1913	if len(w.violations) == 0 || invariantOf(w.violations[0]) != "INV-I1" {
1914	t.Errorf("a broken --public under the formerly tagged process: want INV-I1, got violations %v residuals %v", w.violations, w.residuals)
1915	dump(t, w)
1916	}
1917	})
1918	}
1919
1920	// flatEraFixture is residualFlatEraTamper's setup with the flag on, the
1921	// tamper planted in group target's instance directory instead of shop's: a
1922	// flat tenant on unarmed box 1 plants it, its route moves off, the box is
1923	// armed, and shop and other (a sibling instance) start. It returns box 1.
1924	func flatEraFixture(t *testing.T, target string) (*world, *box) {
1925	w := newWitness()
1926	w.flatEraTamper = true
1927	w.runningEngine(t)
1928	b := w.boxes[1]
1929	if !w.provision(b, "other", "acct/other", "127.0.0.1:9002", vPlain) {
1930	t.Fatalf("fixture: provisioning other refused: %s", w.boxesState())
1931	}
1932	b.Live["shop"], b.Good["shop"] = vPlain, vPlain
1933	if !w.launchUnisolated(b, "flat") {
1934	t.Fatalf("fixture: a flat start on an unarmed box refused: %s", w.boxesState())
1935	}
1936	w.tamper(b, w.newest(b, "flat"), target)
1937	w.moveToNested(b, "flat")
1938	if !w.arm(b) {
1939	t.Fatalf("fixture: arming refused after the flat route moved: %s", w.boxesState())
1940	}
1941	for _, g := range []string{"shop", "other"} {
1942	w.stopGroup(b, g)
1943	if !w.launch(b, g, vPlain, "seed") {
1944	t.Fatalf("fixture: %s did not start: %s", g, w.boxesState())
1945	}
1946	}
1947	w.check()
1948	if len(w.violations) > 0 {
1949	t.Fatalf("fixture: violations %v", w.violations)
1950	}
1951	return w, b
1952	}
1953
1954	// TestFlatEraTamperKeepsUnrelatedViolations: the flat-era residual covers a
1955	// call whose recorded caller is the compromised instance itself, made by its
1956	// own process in its own slice (final review, finding 5). Combined with an
1957	// unrelated mutation, the unrelated breach stays a violation:
1958	// - cgroup-identity off: planted code in other borrows shop's engine
1959	// socket; the engine box records shop, which is not the compromised
1960	// instance;
1961	// - hop-caller-signed off: planted code in shop sends its own socket's call
1962	// with an X-Carlos-Hop-Caller naming another granted app, which the
1963	// engine box takes.
1964	//
1965	// And the positive control: planted code in shop calling through shop's own
1966	// socket is the residual, not a violation.
1967	func TestFlatEraTamperKeepsUnrelatedViolations(t *testing.T) {
1968	t.Run("own socket: the residual", func(t *testing.T) {
1969	w, b := flatEraFixture(t, "shop")
1970	w.engineCall(b, w.newest(b, "shop"), false, "carlos", "shop", eng, "/")
1971	w.check()
1972	if len(w.violations) > 0 || len(w.residuals) != 1 || !strings.HasPrefix(w.residuals[0], "residual:flatEraTamper:") {
1973	t.Errorf("want residual:flatEraTamper and no violation, got violations %v residuals %v", w.violations, w.residuals)
1974	dump(t, w)
1975	}
1976	})
1977	t.Run("cgroup-identity off: a borrowed socket", func(t *testing.T) {
1978	w, b := flatEraFixture(t, "other")
1979	withMutation("cgroup-identity", func() {
1980	w.engineCall(b, w.newest(b, "other"), false, "carlos", "shop", eng, "/")
1981	})
1982	w.check()
1983	if len(w.violations) != 1 || invariantOf(w.violations[0]) != "INV-ID" || len(w.residuals) > 0 {
1984	t.Errorf("want INV-ID and no residual, got violations %v residuals %v", w.violations, w.residuals)
1985	dump(t, w)
1986	}
1987	})
1988	t.Run("hop-caller-signed off: a forged hop caller", func(t *testing.T) {
1989	w, b := flatEraFixture(t, "shop")
1990	w.consoleGrant("acct/tcp/" + eng)
1991	w.pollAll()
1992	forged := callerOf("acct/tcp", eng)
1993	withMutation("hop-caller-signed", func() {
1994	w.placeCall(call{from: b, p: w.newest(b, "shop"), uid: "carlos", host: "shop", engine: eng, path: "/", forged: &forged})
1995	})
1996	w.check()
1997	if len(w.violations) != 1 || invariantOf(w.violations[0]) != "INV-ID" || len(w.residuals) > 0 {
1998	t.Errorf("want INV-ID and no residual, got violations %v residuals %v", w.violations, w.residuals)
1999	dump(t, w)
2000	}
2001	})
2002	}
2003
2004	// TestWitnessesHoldUnmutated: every witness holds with every rule in place.
2005	// A witness that violates unmutated is a model bug, and a witness that
2006	// passes under its mutation for the wrong reason starts here (Review Focus 1).
2007	func TestWitnessesHoldUnmutated(t *testing.T) {
2008	saved := mutated
2009	mutated = ""
2010	defer func() { mutated = saved }()
2011	if len(witnesses) == 0 {
2012	t.Fatal("no witnesses")
2013	}
2014	for _, x := range witnesses {
2015	w := newWitness()
2016	x.run(t, w)
2017	if len(w.violations) > 0 {
2018	t.Errorf("witness %s (needs %q) violates with no mutation: %v", x.rule, x.needs, w.violations)
2019	dump(t, w)
2020	}
2021	}
2022	}
2023
2024	// expectedOutcome is one line of expected-outcomes.txt: `rule missed reason`
2025	// or `rule rare N reason` (hostlife's format, read by mutate.sh).
2026	type expectedOutcome struct {
2027	rule, outcome string
2028	depth int
2029	reason string
2030	}
2031
2032	func readExpectedOutcomes(t *testing.T) []expectedOutcome {
2033	t.Helper()
2034	data, err := os.ReadFile("expected-outcomes.txt")
2035	if err != nil {
2036	t.Fatalf("mutate.sh reads expected-outcomes.txt beside it: %v", err)
2037	}
2038	var out []expectedOutcome
2039	for i, line := range strings.Split(string(data), "\n") {
2040	if strings.HasPrefix(line, "#") || strings.TrimSpace(line) == "" {
2041	continue
2042	}
2043	f := strings.Fields(line)
2044	e := expectedOutcome{rule: f[0]}
2045	if len(f) > 1 {
2046	e.outcome = f[1]
2047	}
2048	rest := f[min(2, len(f)):]
2049	if e.outcome == "rare" {
2050	if len(f) < 3 {
2051	t.Errorf("expected-outcomes.txt:%d: rare needs a seed count: %q", i+1, line)
2052	continue
2053	}
2054	if _, err := fmt.Sscanf(f[2], "%d", &e.depth); err != nil || e.depth <= 0 {
2055	t.Errorf("expected-outcomes.txt:%d: rare needs a positive seed count: %q", i+1, line)
2056	}
2057	rest = f[3:]
2058	}
2059	e.reason = strings.Join(rest, " ")
2060	out = append(out, e)
2061	}
2062	return out
2063	}
2064
2065	// TestEveryRuleHasWitness: each rule in allRules has a witness or a line in
2066	// expected-outcomes.txt that says why it has none or why it is not caught
2067	// alone; every line there is well formed and names a known rule; and a rule
2068	// listed `missed` has no witness that its mutation alone must violate (the
2069	// harness would report it STALE).
2070	func TestEveryRuleHasWitness(t *testing.T) {
2071	known := map[string]bool{}
2072	for _, r := range allRules {
2073	known[r] = true
2074	}
2075	expected := map[string]expectedOutcome{}
2076	for _, e := range readExpectedOutcomes(t) {
2077	if !known[e.rule] {
2078	t.Errorf("expected-outcomes.txt names unknown rule %q", e.rule)
2079	}
2080	if _, dup := expected[e.rule]; dup {
2081	t.Errorf("expected-outcomes.txt lists %q twice", e.rule)
2082	}
2083	if e.outcome != "missed" && e.outcome != "rare" {
2084	t.Errorf("expected-outcomes.txt: %s: outcome %q, want missed or rare N", e.rule, e.outcome)
2085	}
2086	if e.reason == "" {
2087	t.Errorf("expected-outcomes.txt: %s gives no reason", e.rule)
2088	}
2089	expected[e.rule] = e
2090	}
2091	witnessed := map[string]bool{}
2092	for _, x := range witnesses {
2093	witnessed[x.rule] = true
2094	if e, ok := expected[x.rule]; ok && e.outcome == "missed" && x.needs == x.rule {
2095	t.Errorf("%s is listed missed, but a witness must violate under its mutation alone", x.rule)
2096	}
2097	}
2098	for _, r := range allRules {
2099	if !witnessed[r] {
2100	if _, ok := expected[r]; !ok {
2101	t.Errorf("rule %q has neither a witness nor an expected-outcomes.txt line", r)
2102	}
2103	}
2104	}
2105	}
2106