1	import Base
2	import ../../general/rose/type.bend as R
3	import ../../general/rose/ops.bend as RO
4	import ../../general/compound/type.bend as C
5	import ../../general/compound/ops.bend as CO
6	import ../../general/compound/edge/type.bend as E
7	import ./relationship/type.bend as Rel
8	import ./system/type.bend as S
9	import ./system/container/type.bend as Ct
10	import ./system/container/component/type.bend as Co
11	import ./system/deployment/type.bend as D
12	import ./environment/type.bend as En
13	import ./environment/party/type.bend as P
14	import ./environment/external/type.bend as X
15	import ./environment/constraint/type.bend as K
16	import ./system/release/ops.bend as RlO
17	import ./category/type.bend as K2
18	import ./environment/inventory/type.bend as I
19	import ./environment/inventory/ops.bend as InvO
20	import ./environment/agreement/type.bend as G
21	import ./system/deployment/host/type.bend as H
22	import ./system/deployment/nix_darwin/ops.bend as NDO
23	import ./system/deployment/nix_darwin/type.bend as ND
24	import ./system/deployment/nix_darwin/setting/ops.bend as StO
25	import ./type.bend as A
26	
27	# ---- the architecture as a compound graph: the system's tree, the environment's leaves, and every
28	# element's relationships as edges from it ----
29	def uses_edges(+src: String, us: List<&2, Rel.Relationship>) -> List<&2, E.Edge>:
30	  match us:
31	    case []:
32	      []
33	    case u <> rest:
34	      match u:
35	        case Rel.Relationship{d, desc, t, _}:
36	          E.Edge{src, d, desc, t} <> uses_edges(src, rest)
37	
38	def language_name(l: Co.Language) -> String:
39	  match l:
40	    case Co.Bend{}:
41	      "Bend 2"
42	    case Co.C{}:
43	      "C"
44	    case Co.Rust{}:
45	      "Rust"
46	    case Co.TypeScript{}:
47	      "TypeScript"
48	    case Co.JavaScript{}:
49	      "JavaScript"
50	    case Co.Python{}:
51	      "Python"
52	    case Co.Go{}:
53	      "Go"
54	    case Co.Opaque{}:
55	      ""
56	
57	# A container's technology, as drawn: its frameworks and languages, else its vendors.
58	def technology(+vs: List<&2, String>, +fs: List<&2, String>, +ls: List<&2, String>) -> String:
59	  Bool.pick(String, List.is_empty(&2, String, List.append(&2, String, fs, ls)), String.join(vs, ", "), String.join(List.append(&2, String, fs, ls), ", "))
60	
61	def component_roses(cs: List<&2, Co.Component>) -> List<&2, R.Rose<A.Element>>:
62	  match cs:
63	    case []:
64	      []
65	    case c <> rest:
66	      match c:
67	        case Co.Component{k, n, d, l, _}:
68	          R.Rose{k, A.Element{n, d, language_name(l), A.ComponentLevel{}}, []} <> component_roses(rest)
69	
70	def component_edges(cs: List<&2, Co.Component>) -> List<&2, E.Edge>:
71	  match cs:
72	    case []:
73	      []
74	    case c <> rest:
75	      match c:
76	        case Co.Component{k, _, _, _, us}:
77	          List.append(&2, E.Edge, uses_edges(k, us), component_edges(rest))
78	
79	def container_roses(cs: List<&2, Ct.Container>) -> List<&2, R.Rose<A.Element>>:
80	  match cs:
81	    case []:
82	      []
83	    case c <> rest:
84	      match c:
85	        case Ct.Container{k, n, d, _, _, _, _, _, vs, fs, _, ls, _, comps, _}:
86	          R.Rose{k, A.Element{n, d, technology(vs, fs, ls), A.ContainerLevel{}}, component_roses(comps)} <> container_roses(rest)
87	
88	def container_edges(cs: List<&2, Ct.Container>) -> List<&2, E.Edge>:
89	  match cs:
90	    case []:
91	      []
92	    case c <> rest:
93	      match c:
94	        case Ct.Container{+k, _, _, _, _, _, _, _, _, _, _, _, _, comps, us}:
95	          List.append(&2, E.Edge, uses_edges(k, us), List.append(&2, E.Edge, component_edges(comps), container_edges(rest)))
96	
97	def party_rose(p: P.Party) -> R.Rose<A.Element>:
98	  match p:
99	    case P.Human{k, n, d, _}:
100	      R.Rose{k, A.Element{n, d, "", A.PersonLevel{}}, []}
101	    case P.Organization{k, n, d, _, _}:
102	      R.Rose{k, A.Element{n, d, "", A.PersonLevel{}}, []}
103	    case P.Team{k, n, d, _, _}:
104	      R.Rose{k, A.Element{n, d, "", A.PersonLevel{}}, []}
105	
106	def party_edges(p: P.Party) -> List<&2, E.Edge>:
107	  match p:
108	    case P.Human{k, _, _, us}:
109	      uses_edges(k, us)
110	    case P.Organization{k, _, _, _, us}:
111	      uses_edges(k, us)
112	    case P.Team{k, _, _, _, us}:
113	      uses_edges(k, us)
114	
115	def parties_roses(ps: List<&2, P.Party>) -> List<&2, R.Rose<A.Element>>:
116	  match ps:
117	    case []:
118	      []
119	    case p <> rest:
120	      party_rose(p) <> parties_roses(rest)
121	
122	def parties_edges(ps: List<&2, P.Party>) -> List<&2, E.Edge>:
123	  match ps:
124	    case []:
125	      []
126	    case p <> rest:
127	      List.append(&2, E.Edge, party_edges(p), parties_edges(rest))
128	
129	def external_roses(xs: List<&2, X.External>) -> List<&2, R.Rose<A.Element>>:
130	  match xs:
131	    case []:
132	      []
133	    case x <> rest:
134	      match x:
135	        case X.External{k, n, d, _, _, _, _, _}:
136	          R.Rose{k, A.Element{n, d, "", A.ExternalLevel{}}, []} <> external_roses(rest)
137	
138	def external_edges(xs: List<&2, X.External>) -> List<&2, E.Edge>:
139	  match xs:
140	    case []:
141	      []
142	    case x <> rest:
143	      match x:
144	        case X.External{k, _, _, _, _, _, _, us}:
145	          List.append(&2, E.Edge, uses_edges(k, us), external_edges(rest))
146	
147	def with_env(sys: R.Rose<A.Element>, +cs: List<&2, Ct.Container>, env: En.Environment) -> C.Compound<A.Element>:
148	  match env:
149	    case En.Environment{+ps, +xs, _, _, _}:
150	      C.Compound{sys <> List.append(&2, R.Rose<A.Element>, parties_roses(ps), external_roses(xs)),
151	        List.append(&2, E.Edge, container_edges(cs), List.append(&2, E.Edge, parties_edges(ps), external_edges(xs)))}
152	
153	def to_compound(a: A.Architecture) -> C.Compound<A.Element>:
154	  match a:
155	    case A.Architecture{s, env}:
156	      match s:
157	        case S.System{k, n, d, +cs, _, _}:
158	          with_env(R.Rose{k, A.Element{n, d, "", A.SystemLevel{}}, container_roses(cs)}, cs, env)
159	
160	# ---- looking things up ----
161	def system(a: A.Architecture) -> S.System:
162	  match a:
163	    case A.Architecture{s, _}:
164	      s
165	
166	def system_key(a: A.Architecture) -> String:
167	  match a:
168	    case A.Architecture{s, _}:
169	      match s:
170	        case S.System{k, _, _, _, _, _}:
171	          k
172	
173	def containers(a: A.Architecture) -> List<&2, Ct.Container>:
174	  match a:
175	    case A.Architecture{s, _}:
176	      match s:
177	        case S.System{_, _, _, cs, _, _}:
178	          cs
179	
180	def deployment(a: A.Architecture) -> D.Deployment:
181	  match a:
182	    case A.Architecture{s, _}:
183	      match s:
184	        case S.System{_, _, _, _, dep, _}:
185	          dep
186	
187	def deployment_nodes(d: D.Deployment) -> List<&2, D.Node>:
188	  match d:
189	    case D.Deployment{_, _, _, ns}:
190	      ns
191	
192	# The machines, nested.
193	def nodes(a: A.Architecture) -> List<&2, D.Node>:
194	  deployment_nodes(deployment(a))
195	
196	def keys(a: A.Architecture) -> List<&2, String>:
197	  CO.keys(A.Element, to_compound(a))
198	
199	def container_keys(cs: List<&2, Ct.Container>) -> List<&2, String>:
200	  match cs:
201	    case []:
202	      []
203	    case c <> rest:
204	      match c:
205	        case Ct.Container{k, _, _, _, _, _, _, _, _, _, _, _, _, _, _}:
206	          k <> container_keys(rest)
207	
208	def component_keys(cs: List<&2, Co.Component>) -> List<&2, String>:
209	  match cs:
210	    case []:
211	      []
212	    case c <> rest:
213	      match c:
214	        case Co.Component{k, _, _, _, _}:
215	          k <> component_keys(rest)
216	
217	# Every component key in the system.
218	def all_component_keys(cs: List<&2, Ct.Container>) -> List<&2, String>:
219	  match cs:
220	    case []:
221	      []
222	    case c <> rest:
223	      match c:
224	        case Ct.Container{_, _, _, _, _, _, _, _, _, _, _, _, _, comps, _}:
225	          List.append(&2, String, component_keys(comps), all_component_keys(rest))
226	
227	# The components inside one container.
228	def components_of(+k: String, cs: List<&2, Ct.Container>) -> List<&2, String>:
229	  match cs:
230	    case []:
231	      []
232	    case c <> rest:
233	      match c:
234	        case Ct.Container{ck, _, _, _, _, _, _, _, _, _, _, _, _, comps, _}:
235	          Bool.pick(List<&2, String>, String.eq(k, ck), component_keys(comps), components_of(k, rest))
236	
237	def environment_keys(a: A.Architecture) -> List<&2, String>:
238	  match a:
239	    case A.Architecture{_, env}:
240	      match env:
241	        case En.Environment{ps, xs, _, _, _}:
242	          RO.keys(A.Element, List.append(&2, R.Rose<A.Element>, parties_roses(ps), external_roses(xs)))
243	
244	# ---- well formed: keys are unique, every relationship and every instance names something that exists ----
245	def instances(ns: List<&2, D.Node>) -> List<&2, String>:
246	  match ns:
247	    case []:
248	      []
249	    case n <> rest:
250	      match n:
251	        case D.Node{_, _, _, _, _, _, kids, ins}:
252	          List.append(&2, String, ins, List.append(&2, String, instances(kids), instances(rest)))
253	
254	def all_listed(xs: List<&2, String>, +ks: List<&2, String>) -> Bool:
255	  match xs:
256	    case []:
257	      True{}
258	    case x <> rest:
259	      CO.has(ks, x) && all_listed(rest, ks)
260	
261	def compound_ok(+c: C.Compound<A.Element>) -> Bool:
262	  CO.resolves(A.Element, c) && CO.unique(A.Element, c)
263	
264	def well_formed(+a: A.Architecture) -> Bool:
265	  compound_ok(to_compound(a)) && all_listed(instances(nodes(a)), container_keys(containers(a)))
266	
267	# ---- only our own containers are opened up into components ----
268	def ours(o: Ct.Ownership) -> Bool:
269	  match o:
270	    case Ct.Ours{}:
271	      True{}
272	    case Ct.Theirs{}:
273	      False{}
274	
275	def components_ours(cs: List<&2, Ct.Container>) -> Bool:
276	  match cs:
277	    case []:
278	      True{}
279	    case c <> rest:
280	      match c:
281	        case Ct.Container{_, _, _, _, o, _, _, _, _, _, _, _, _, comps, _}:
282	          (List.is_empty(&2, Co.Component, comps) || ours(o)) && components_ours(rest)
283	
284	# ---- on a server, everything is reachable only from the machine itself or over the tailnet ----
285	def private(e: Ct.Exposure) -> Bool:
286	  match e:
287	    case Ct.Local{}:
288	      True{}
289	    case Ct.Tailnet{}:
290	      True{}
291	    case _:
292	      False{}
293	
294	def exposure_private(+k: String, cs: List<&2, Ct.Container>) -> Bool:
295	  match cs:
296	    case []:
297	      True{}
298	    case c <> rest:
299	      match c:
300	        case Ct.Container{ck, _, _, _, _, e, _, _, _, _, _, _, _, _, _}:
301	          Bool.pick(Bool, String.eq(k, ck), private(e), exposure_private(k, rest))
302	
303	def all_private(ins: List<&2, String>, +cs: List<&2, Ct.Container>) -> Bool:
304	  match ins:
305	    case []:
306	      True{}
307	    case i <> rest:
308	      exposure_private(i, cs) && all_private(rest, cs)
309	
310	def is_server(r: D.Role) -> Bool:
311	  match r:
312	    case D.Server{}:
313	      True{}
314	    case D.Device{}:
315	      False{}
316	
317	def nodes_private(ns: List<&2, D.Node>, +cs: List<&2, Ct.Container>) -> Bool:
318	  match ns:
319	    case []:
320	      True{}
321	    case n <> rest:
322	      match n:
323	        case D.Node{_, _, _, r, _, _, kids, ins}:
324	          (Bool.not(is_server(r)) || all_private(ins, cs)) && nodes_private(kids, cs) && nodes_private(rest, cs)
325	
326	def servers_private(+a: A.Architecture) -> Bool:
327	  nodes_private(nodes(a), containers(a))
328	
329	# ---- open source: a system its environment requires to be open source publishes from a public repository ----
330	def open_source_required(ks: List<&2, K.Constraint>) -> Bool:
331	  match ks:
332	    case []:
333	      False{}
334	    case k <> rest:
335	      match k:
336	        case K.OpenSource{}:
337	          True{}
338	        case K.RunsOn{_}:
339	          open_source_required(rest)
340	
341	def open_source(a: A.Architecture) -> Bool:
342	  match a:
343	    case A.Architecture{s, env}:
344	      match s env:
345	        case S.System{_, _, _, _, _, r} En.Environment{_, _, ks, _, _}:
346	          Bool.not(open_source_required(ks)) || RlO.is_public(r)
347	
348	# ---- where each key runs: the containers on server nodes and on device nodes ----
349	def is_device(r: D.Role) -> Bool:
350	  match r:
351	    case D.Device{}:
352	      True{}
353	    case D.Server{}:
354	      False{}
355	
356	def keep_all(c: Bool, xs: List<&2, String>, rest: List<&2, String>) -> List<&2, String>:
357	  match c:
358	    case True{}:
359	      List.append(&2, String, xs, rest)
360	    case False{}:
361	      rest
362	
363	def on_servers(ns: List<&2, D.Node>) -> List<&2, String>:
364	  match ns:
365	    case []:
366	      []
367	    case n <> rest:
368	      match n:
369	        case D.Node{_, _, _, r, _, _, kids, ins}:
370	          keep_all(is_server(r), ins, List.append(&2, String, on_servers(kids), on_servers(rest)))
371	
372	def on_devices(ns: List<&2, D.Node>) -> List<&2, String>:
373	  match ns:
374	    case []:
375	      []
376	    case n <> rest:
377	      match n:
378	        case D.Node{_, _, _, r, _, _, kids, ins}:
379	          keep_all(is_device(r), ins, List.append(&2, String, on_devices(kids), on_devices(rest)))
380	
381	# The container a key belongs to: itself, or the one its component sits in, else the key itself.
382	def home(+k: String, cs: List<&2, Ct.Container>) -> String:
383	  match cs:
384	    case []:
385	      k
386	    case c <> rest:
387	      match c:
388	        case Ct.Container{+ck, _, _, _, _, _, _, _, _, _, _, _, _, comps, _}:
389	          Bool.pick(String, String.eq(k, ck) || CO.has(component_keys(comps), k), ck, home(k, rest))
390	
391	def exposure_of(+k: String, cs: List<&2, Ct.Container>) -> Ct.Exposure:
392	  match cs:
393	    case []:
394	      Ct.Public{}
395	    case c <> rest:
396	      match c:
397	        case Ct.Container{ck, _, _, _, _, e, _, _, _, _, _, _, _, _, _}:
398	          Bool.pick(Ct.Exposure, String.eq(k, ck), e, exposure_of(k, rest))
399	
400	def is_tailnet(e: Ct.Exposure) -> Bool:
401	  match e:
402	    case Ct.Tailnet{}:
403	      True{}
404	    case _:
405	      False{}
406	
407	def is_local(e: Ct.Exposure) -> Bool:
408	  match e:
409	    case Ct.Local{}:
410	      True{}
411	    case _:
412	      False{}
413	
414	def edges(a: A.Architecture) -> List<&2, E.Edge>:
415	  CO.edges(A.Element, to_compound(a))
416	
417	# ---- a device reaches a server only over the tailnet ----
418	def via_tailnet(es: List<&2, E.Edge>, +cs: List<&2, Ct.Container>, +servers: List<&2, String>, +devices: List<&2, String>) -> Bool:
419	  match es:
420	    case []:
421	      True{}
422	    case e <> rest:
423	      match e:
424	        case E.Edge{x, +y, _, _}:
425	          (Bool.not(CO.has(devices, home(x, cs)) && CO.has(servers, home(y, cs))) || is_tailnet(exposure_of(home(y, cs), cs))) &&
426	            via_tailnet(rest, cs, servers, devices)
427	
428	def devices_via_tailnet(+a: A.Architecture) -> Bool:
429	  via_tailnet(edges(a), containers(a), on_servers(nodes(a)), on_devices(nodes(a)))
430	
431	# ---- on a server, a container is on the tailnet exactly when a device reaches it, else local ----
432	def reached(+k: String, es: List<&2, E.Edge>, +cs: List<&2, Ct.Container>, +devices: List<&2, String>) -> Bool:
433	  match es:
434	    case []:
435	      False{}
436	    case e <> rest:
437	      match e:
438	        case E.Edge{x, y, _, _}:
439	          (CO.has(devices, home(x, cs)) && String.eq(home(y, cs), k)) || reached(k, rest, cs, devices)
440	
441	def follows_reach(r: Bool, e: Ct.Exposure) -> Bool:
442	  match r:
443	    case True{}:
444	      is_tailnet(e)
445	    case False{}:
446	      is_local(e)
447	
448	def reach_ok(ks: List<&2, String>, +a: A.Architecture) -> Bool:
449	  match ks:
450	    case []:
451	      True{}
452	    case +k <> rest:
453	      follows_reach(reached(k, edges(a), containers(a), on_devices(nodes(a))), exposure_of(k, containers(a))) && reach_ok(rest, a)
454	
455	def exposure_follows_reach(+a: A.Architecture) -> Bool:
456	  reach_ok(on_servers(nodes(a)), a)
457	
458	# ---- capabilities: who provides each, and how many do ----
459	def cap_eq(a: K2.Capability, b: K2.Capability) -> Bool:
460	  match a b:
461	    case K2.Hosting{} K2.Hosting{}:
462	      True{}
463	    case K2.Realtime{} K2.Realtime{}:
464	      True{}
465	    case K2.BlobStore{} K2.BlobStore{}:
466	      True{}
467	    case K2.Observability{} K2.Observability{}:
468	      True{}
469	    case _ _:
470	      False{}
471	
472	def has_cap(+want: K2.Capability, cs: List<&2, K2.Capability>) -> Bool:
473	  match cs:
474	    case []:
475	      False{}
476	    case c <> rest:
477	      cap_eq(want, c) || has_cap(want, rest)
478	
479	def one_if(b: Bool) -> Nat:
480	  match b:
481	    case True{}:
482	      1n
483	    case False{}:
484	      0n
485	
486	def container_providers(+want: K2.Capability, cs: List<&2, Ct.Container>) -> List<&2, String>:
487	  match cs:
488	    case []:
489	      []
490	    case c <> rest:
491	      match c:
492	        case Ct.Container{k, _, _, _, _, _, caps, _, _, _, _, _, _, _, _}:
493	          keep_all(has_cap(want, caps), [k], container_providers(want, rest))
494	
495	def external_providers(+want: K2.Capability, xs: List<&2, X.External>) -> List<&2, String>:
496	  match xs:
497	    case []:
498	      []
499	    case x <> rest:
500	      match x:
501	        case X.External{k, _, _, _, caps, _, _, _}:
502	          keep_all(has_cap(want, caps), [k], external_providers(want, rest))
503	
504	def externals(a: A.Architecture) -> List<&2, X.External>:
505	  match a:
506	    case A.Architecture{_, env}:
507	      match env:
508	        case En.Environment{_, xs, _, _, _}:
509	          xs
510	
511	# The containers and outside systems that provide a capability.
512	def providers(+want: K2.Capability, +a: A.Architecture) -> List<&2, String>:
513	  List.append(&2, String, container_providers(want, containers(a)), external_providers(want, externals(a)))
514	
515	def provided(+want: K2.Capability, +a: A.Architecture) -> Nat:
516	  List.length(&2, String, providers(want, a))
517	
518	# How many containers host the app privately: Hosting, on the tailnet.
519	def private_hosts(cs: List<&2, Ct.Container>) -> Nat:
520	  match cs:
521	    case []:
522	      0n
523	    case c <> rest:
524	      match c:
525	        case Ct.Container{_, _, _, _, _, e, +caps, _, _, _, _, _, _, _, _}:
526	          Nat.add(one_if(has_cap(K2.Hosting{}, caps) && is_tailnet(e)), private_hosts(rest))
527	
528	def private_hosting(+a: A.Architecture) -> Nat:
529	  private_hosts(containers(a))
530	
531	def is_data_api(c: K2.Category) -> Bool:
532	  match c:
533	    case K2.DataApi{}:
534	      True{}
535	    case _:
536	      False{}
537	
538	# The system's own data APIs. "Exactly one" means one store.
539	def data_apis(cs: List<&2, Ct.Container>) -> Nat:
540	  match cs:
541	    case []:
542	      0n
543	    case c <> rest:
544	      match c:
545	        case Ct.Container{_, _, _, cat, _, _, _, _, _, _, _, _, _, _, _}:
546	          Nat.add(one_if(is_data_api(cat)), data_apis(rest))
547	
548	def own_data_apis(+a: A.Architecture) -> Nat:
549	  data_apis(containers(a))
550	
551	# A data API may also host the app only while it is private.
552	def shared_ok(c: Ct.Container) -> Bool:
553	  match c:
554	    case Ct.Container{_, _, _, cat, _, +e, +caps, _, _, _, _, _, _, _, _}:
555	      Bool.not(is_data_api(cat) && has_cap(K2.Hosting{}, caps)) || is_tailnet(e) || is_local(e)
556	
557	def all_shared_ok(cs: List<&2, Ct.Container>) -> Bool:
558	  match cs:
559	    case []:
560	      True{}
561	    case c <> rest:
562	      shared_ok(c) && all_shared_ok(rest)
563	
564	def shared_hosting_private(+a: A.Architecture) -> Bool:
565	  all_shared_ok(containers(a))
566	
567	# ---- observed: everything we build reports to an observability provider ----
568	def reports(+k: String, es: List<&2, E.Edge>, +cs: List<&2, Ct.Container>, +obs: List<&2, String>) -> Bool:
569	  match es:
570	    case []:
571	      False{}
572	    case e <> rest:
573	      match e:
574	        case E.Edge{x, y, _, _}:
575	          (String.eq(home(x, cs), k) && CO.has(obs, y)) || reports(k, rest, cs, obs)
576	
577	def built_observed(cs: List<&2, Ct.Container>, +a: A.Architecture) -> Bool:
578	  match cs:
579	    case []:
580	      True{}
581	    case c <> rest:
582	      match c:
583	        case Ct.Container{+k, _, _, _, o, _, _, +src, _, _, _, _, _, _, _}:
584	          (Bool.not(ours(o) && Bool.not(String.is_empty(src))) || reports(k, edges(a), containers(a), providers(K2.Observability{}, a))) &&
585	            built_observed(rest, a)
586	
587	def observed(+a: A.Architecture) -> Bool:
588	  built_observed(containers(a), a)
589	
590	# ---- the environment's inventory and agreement ----
591	def inventory(a: A.Architecture) -> I.Inventory:
592	  match a:
593	    case A.Architecture{_, env}:
594	      match env:
595	        case En.Environment{_, _, _, inv, _}:
596	          inv
597	
598	def agreement(a: A.Architecture) -> G.Agreement:
599	  match a:
600	    case A.Architecture{_, env}:
601	      match env:
602	        case En.Environment{_, _, _, _, ag}:
603	          ag
604	
605	# ---- every server and device is the owner's, or on its vendor's cloud ----
606	def host_ok(h: H.Host, +name: String, +inv: I.Inventory) -> Bool:
607	  match h:
608	    case H.Owned{k}:
609	      InvO.owns(inv, k, name)
610	    case H.Cloud{p}:
611	      InvO.cloud_ok(inv, p)
612	    case H.Other{}:
613	      False{}
614	
615	def nodes_owned(ns: List<&2, D.Node>, +inv: I.Inventory) -> Bool:
616	  match ns:
617	    case []:
618	      True{}
619	    case n <> rest:
620	      match n:
621	        case D.Node{_, +name, _, _, h, _, kids, _}:
622	          host_ok(h, name, inv) && nodes_owned(kids, inv) && nodes_owned(rest, inv)
623	
624	def owned_nodes(+a: A.Architecture) -> Bool:
625	  nodes_owned(nodes(a), inventory(a))
626	
627	# ---- every nix-darwin node: its serve ports are distinct, its services and serves run what it hosts, a
628	# container on it is on the tailnet exactly when it is served, and its listeners belong to something ----
629	def firewall_typed(nd: ND.NixDarwin) -> Bool:
630	  match nd:
631	    case ND.NixDarwin{_, _, _, _, _, st, _, _, _, _, _, _, _, _}:
632	      StO.firewall_typed(st)
633	
634	def node_keys(ns: List<&2, D.Node>) -> List<&2, String>:
635	  match ns:
636	    case []:
637	      []
638	    case n <> rest:
639	      match n:
640	        case D.Node{k, _, _, _, _, _, kids, _}:
641	          k <> List.append(&2, String, node_keys(kids), node_keys(rest))
642	
643	def darwin_ok(p: D.Platform, +ins: List<&2, String>, +a: A.Architecture) -> Bool:
644	  match p:
645	    case D.Darwin{+nd}:
646	      firewall_typed(nd) && NDO.serve_ports_distinct(nd) && NDO.services_on(nd, ins) && NDO.exposure_honest(nd, containers(a), ins) &&
647	        NDO.listeners_belong(nd, List.append(&2, String, container_keys(containers(a)), node_keys(nodes(a))))
648	    case _:
649	      True{}
650	
651	def darwin_nodes_ok(ns: List<&2, D.Node>, +a: A.Architecture) -> Bool:
652	  match ns:
653	    case []:
654	      True{}
655	    case n <> rest:
656	      match n:
657	        case D.Node{_, _, _, _, _, p, kids, ins}:
658	          darwin_ok(p, ins, a) && darwin_nodes_ok(kids, a) && darwin_nodes_ok(rest, a)
659	
660	def nix_darwin_ok(+a: A.Architecture) -> Bool:
661	  darwin_nodes_ok(nodes(a), a)