1	import Base
2	
3	# Arc: a system's architecture as types, in two hierarchies over the same containers.
4	#   Where it runs: node -> container -> part.
5	#   What it is:    system -> container -> part.
6	# Keys work like foreign keys: a container names its host node (`on`), a part its container (`in`)
7	# and execution node (`on`), and a link two keys. A project states its laws with the predicates
8	# below; the compiler proves them.
9	
10	# ---- vocabulary ----
11	# UserDevice: a user's own device. Server: a machine the project runs. Overlay: the private
12	# (overlay) network between them. Outside: someone else's servers.
13	type NodeRole is Data:
14	  UserDevice{}
15	  Server{}
16	  Overlay{}
17	  Outside{}
18	
19	type PhysicalDevice is Data:
20	  PhysicalDevice{key: String, name: String, platform: String}
21	
22	type Vendor is Data:
23	  Vendor{name: String, cloud: String}
24	
25	type Org is Data:
26	  Org{name: String, vendor: Vendor, devices: List<&2, PhysicalDevice>}
27	
28	type Host is Data:
29	  Owned{device: String}
30	  Cloud{provider: String}
31	  Other{}
32	
33	type Node is Data:
34	  Node{key: String, name: String, role: NodeRole, host: Host}
35	
36	# What a container is. The list is closed: something that is none of these is not a container.
37	# Client: the app, on the user's device. The private overlay is a node, not a container.
38	# DataApi: answers queries on records and changes them.
39	# Harness: an agent harness, the loop around a model (tools, context, threads), driven over its remote-control API.
40	# Proxy: forwards connections to another container, adding what it lacks, such as TLS or authentication.
41	# ModelApi: answers model calls. Cli: a command a person runs. Worker: has no API of its own; it
42	# only moves data between data APIs, so it is the first thing to fold into a data API's own actions.
43	type ContainerKind is Data:
44	  Client{}
45	  DataApi{}
46	  Harness{}
47	  Proxy{}
48	  ModelApi{}
49	  Cli{}
50	  Worker{}
51	
52	# Whether the project builds and runs it, or uses it as it is.
53	type Owner is Data:
54	  Ours{}
55	  Theirs{}
56	
57	# Who can reach it: its own machine (127.0.0.1), the local network, the overlay, the device it is on, anyone.
58	type Exposure is Data:
59	  Local{}
60	  Lan{}
61	  Tailnet{}
62	  Device{}
63	  Public{}
64	
65	# What a container provides. Hosting is serving the app itself (its HTML and scripts); a data API
66	# may also host the app only while it is private (shared_hosting_ok). Observability is receiving
67	# a running container's errors, traces and structured logs.
68	type Cap is Data:
69	  Hosting{}
70	  PrivateHosting{}
71	  Realtime{}
72	  BlobStore{}
73	  Observability{}
74	
75	type Lang is Data:
76	  Bend{}
77	  C{}
78	  Rust{}
79	  TypeScript{}
80	  JavaScript{}
81	  Python{}
82	  Opaque{}
83	
84	type Container is Data:
85	  Container{key: String, name: String, kind: ContainerKind, owner: Owner, on: String, exposure: Exposure, caps: List<&2, Cap>, source: String, vendors: List<&2, String>, frameworks: List<&2, String>, libraries: List<&2, String>, languages: List<&2, String>}
86	
87	type Part is Data:
88	  Part{key: String, name: String, lang: Lang, in: String, on: String}
89	
90	# A talks-to edge between two containers or parts, by key.
91	type Link is Data:
92	  Link{src: String, dst: String, label: String, live: Bool}
93	
94	type System is Data:
95	  System{org: Org, nodes: List<&2, Node>, containers: List<&2, Container>, parts: List<&2, Part>, links: List<&2, Link>}
96	
97	# ---- access ----
98	def org(s: System) -> Org:
99	  match s:
100	    case System{o, _, _, _, _}:
101	      o
102	
103	def nodes(s: System) -> List<&2, Node>:
104	  match s:
105	    case System{_, n, _, _, _}:
106	      n
107	
108	def containers(s: System) -> List<&2, Container>:
109	  match s:
110	    case System{_, _, c, _, _}:
111	      c
112	
113	def parts(s: System) -> List<&2, Part>:
114	  match s:
115	    case System{_, _, _, p, _}:
116	      p
117	
118	def links(s: System) -> List<&2, Link>:
119	  match s:
120	    case System{_, _, _, _, l}:
121	      l
122	
123	def nkey(n: Node) -> String:
124	  match n:
125	    case Node{k, _, _, _}:
126	      k
127	
128	def ckey(c: Container) -> String:
129	  match c:
130	    case Container{k, _, _, _, _, _, _, _, _, _, _, _}:
131	      k
132	
133	def con(c: Container) -> String:
134	  match c:
135	    case Container{_, _, _, _, o, _, _, _, _, _, _, _}:
136	      o
137	
138	def caps(c: Container) -> List<&2, Cap>:
139	  match c:
140	    case Container{_, _, _, _, _, _, cs, _, _, _, _, _}:
141	      cs
142	
143	def pkey(p: Part) -> String:
144	  match p:
145	    case Part{k, _, _, _, _}:
146	      k
147	
148	def pin(p: Part) -> String:
149	  match p:
150	    case Part{_, _, _, i, _}:
151	      i
152	
153	def pon(p: Part) -> String:
154	  match p:
155	    case Part{_, _, _, _, on}:
156	      on
157	
158	def nkeys(xs: List<&2, Node>) -> List<&2, String>:
159	  match xs:
160	    case []:
161	      []
162	    case n <> rest:
163	      nkey(n) <> nkeys(rest)
164	
165	def ckeys(xs: List<&2, Container>) -> List<&2, String>:
166	  match xs:
167	    case []:
168	      []
169	    case c <> rest:
170	      ckey(c) <> ckeys(rest)
171	
172	def pkeys(xs: List<&2, Part>) -> List<&2, String>:
173	  match xs:
174	    case []:
175	      []
176	    case p <> rest:
177	      pkey(p) <> pkeys(rest)
178	
179	# Keys links may name: containers and parts.
180	def keys(+s: System) -> List<&2, String>:
181	  List.append(&2, String, ckeys(containers(s)), pkeys(parts(s)))
182	
183	# ---- predicates on the vocabulary ----
184	def is_server(r: NodeRole) -> Bool:
185	  match r:
186	    case Server{}:
187	      True{}
188	    case _:
189	      False{}
190	
191	def is_outside(r: NodeRole) -> Bool:
192	  match r:
193	    case Outside{}:
194	      True{}
195	    case _:
196	      False{}
197	
198	def is_device(r: NodeRole) -> Bool:
199	  match r:
200	    case UserDevice{}:
201	      True{}
202	    case _:
203	      False{}
204	
205	def is_overlay(r: NodeRole) -> Bool:
206	  match r:
207	    case Overlay{}:
208	      True{}
209	    case _:
210	      False{}
211	
212	def one_if(b: Bool) -> Nat:
213	  match b:
214	    case True{}:
215	      1n
216	    case False{}:
217	      0n
218	
219	def overlay_nodes.go(xs: List<&2, Node>) -> Nat:
220	  match xs:
221	    case []:
222	      0n
223	    case n <> rest:
224	      match n:
225	        case Node{_, _, role, _}:
226	          Nat.add(one_if(is_overlay(role)), overlay_nodes.go(rest))
227	
228	# Private access is represented by exactly one Overlay node.
229	def overlay_nodes(+s: System) -> Nat:
230	  overlay_nodes.go(nodes(s))
231	
232	def is_client(k: ContainerKind) -> Bool:
233	  match k:
234	    case Client{}:
235	      True{}
236	    case _:
237	      False{}
238	
239	def is_data_api(k: ContainerKind) -> Bool:
240	  match k:
241	    case DataApi{}:
242	      True{}
243	    case _:
244	      False{}
245	
246	def is_ours(o: Owner) -> Bool:
247	  match o:
248	    case Ours{}:
249	      True{}
250	    case Theirs{}:
251	      False{}
252	
253	def is_local(e: Exposure) -> Bool:
254	  match e:
255	    case Local{}:
256	      True{}
257	    case _:
258	      False{}
259	
260	def is_tailnet(e: Exposure) -> Bool:
261	  match e:
262	    case Tailnet{}:
263	      True{}
264	    case _:
265	      False{}
266	
267	def is_rust(l: Lang) -> Bool:
268	  match l:
269	    case Rust{}:
270	      True{}
271	    case _:
272	      False{}
273	
274	# ---- keys, like foreign keys ----
275	def str_eq(a: String, b: String) -> Bool:
276	  String.eq(a, b)
277	
278	def has(+s: String, xs: List<&2, String>) -> Bool:
279	  match xs:
280	    case []:
281	      False{}
282	    case x <> rest:
283	      str_eq(s, x) || has(s, rest)
284	
285	def owned_device(+key: String, +name: String, xs: List<&2, PhysicalDevice>) -> Bool:
286	  match xs:
287	    case []:
288	      False{}
289	    case PhysicalDevice{k, n, _} <> rest:
290	      (str_eq(key, k) && str_eq(name, n)) || owned_device(key, name, rest)
291	
292	def host_in_inventory(h: Host, name: String, o: Org) -> Bool:
293	  match h o:
294	    case Owned{key} Org{_, _, devices}:
295	      owned_device(key, name, devices)
296	    case Cloud{provider} Org{_, Vendor{_, cloud}, _}:
297	      str_eq(provider, cloud)
298	    case Other{} _:
299	      False{}
300	
301	def node_owned(n: Node, +o: Org) -> Bool:
302	  match n:
303	    case Node{_, name, +role, host}:
304	      Bool.not(is_server(role) || is_device(role)) || host_in_inventory(host, name, o)
305	
306	def owned_nodes.go(xs: List<&2, Node>, +o: Org) -> Bool:
307	  match xs:
308	    case []:
309	      True{}
310	    case n <> rest:
311	      node_owned(n, o) && owned_nodes.go(rest, o)
312	
313	# Every server and user device is in the owner's inventory or on its vendor's cloud.
314	def owned_nodes(+s: System) -> Bool:
315	  owned_nodes.go(nodes(s), org(s))
316	
317	def pick_str(c: Bool, a: String, b: String) -> String:
318	  match c:
319	    case True{}:
320	      a
321	    case False{}:
322	      b
323	
324	# No key names two things.
325	def distinct_keys(xs: List<&2, String>) -> Bool:
326	  match xs:
327	    case []:
328	      True{}
329	    case +k <> +rest:
330	      Bool.not(has(k, rest)) && distinct_keys(rest)
331	
332	# Every key in `xs` names something in `ks`.
333	def all_in(xs: List<&2, String>, +ks: List<&2, String>) -> Bool:
334	  match xs:
335	    case []:
336	      True{}
337	    case x <> rest:
338	      has(x, ks) && all_in(rest, ks)
339	
340	def part_ins(xs: List<&2, Part>) -> List<&2, String>:
341	  match xs:
342	    case []:
343	      []
344	    case p <> rest:
345	      pin(p) <> part_ins(rest)
346	
347	def part_ons(xs: List<&2, Part>) -> List<&2, String>:
348	  match xs:
349	    case []:
350	      []
351	    case p <> rest:
352	      pon(p) <> part_ons(rest)
353	
354	def container_ons(xs: List<&2, Container>) -> List<&2, String>:
355	  match xs:
356	    case []:
357	      []
358	    case c <> rest:
359	      con(c) <> container_ons(rest)
360	
361	def link_ends(xs: List<&2, Link>) -> List<&2, String>:
362	  match xs:
363	    case []:
364	      []
365	    case l <> rest:
366	      match l:
367	        case Link{a, b, _, _}:
368	          a <> b <> link_ends(rest)
369	
370	# The system is well formed: node keys and container/part keys are unique, every container is on
371	# a node, every part in a container, and every link joins two things that exist.
372	def well_formed(+s: System) -> Bool:
373	  distinct_keys(nkeys(nodes(s))) && distinct_keys(keys(s)) &&
374	  all_in(container_ons(containers(s)), nkeys(nodes(s))) &&
375	  all_in(part_ins(parts(s)), ckeys(containers(s))) &&
376	  all_in(part_ons(parts(s)), nkeys(nodes(s))) &&
377	  all_in(link_ends(links(s)), keys(s))
378	
379	# ---- looking things up ----
380	def part_home(+k: String, xs: List<&2, Part>) -> String:
381	  match xs:
382	    case []:
383	      ""
384	    case +p <> rest:
385	      pick_str(str_eq(k, pkey(p)), pin(p), part_home(k, rest))
386	
387	# The container a key belongs to: itself, or the one its part sits in.
388	def home(+k: String, +s: System) -> String:
389	  pick_str(has(k, ckeys(containers(s))), k, part_home(k, parts(s)))
390	
391	def none() -> Container:
392	  Container{"", "", Worker{}, Theirs{}, "", Public{}, [], "", [], [], [], []}
393	
394	def pick_c(hit: Bool, c: Container, other: Container) -> Container:
395	  match hit:
396	    case True{}:
397	      c
398	    case False{}:
399	      other
400	
401	# The container with key `k` (an empty one when `k` is unknown; well_formed rules that out).
402	def container(+k: String, xs: List<&2, Container>) -> Container:
403	  match xs:
404	    case []:
405	      none()
406	    case +c <> rest:
407	      pick_c(str_eq(k, ckey(c)), c, container(k, rest))
408	
409	def pick_r(hit: Bool, r: NodeRole, other: NodeRole) -> NodeRole:
410	  match hit:
411	    case True{}:
412	      r
413	    case False{}:
414	      other
415	
416	def node_role(+k: String, xs: List<&2, Node>) -> NodeRole:
417	  match xs:
418	    case []:
419	      Outside{}
420	    case n <> rest:
421	      match n:
422	        case Node{nk, _, r, _}:
423	          pick_r(str_eq(k, nk), r, node_role(k, rest))
424	
425	def part_node(+k: String, xs: List<&2, Part>) -> String:
426	  match xs:
427	    case []:
428	      ""
429	    case +p <> rest:
430	      pick_str(str_eq(k, pkey(p)), pon(p), part_node(k, rest))
431	
432	# The node a container or part runs on, and its role.
433	def node_of(+k: String, +s: System) -> String:
434	  pick_str(has(k, pkeys(parts(s))), part_node(k, parts(s)), con(container(home(k, s), containers(s))))
435	
436	def role_of(+k: String, +s: System) -> NodeRole:
437	  node_role(node_of(k, s), nodes(s))
438	
439	def container_exposure(c: Container) -> Exposure:
440	  match c:
441	    case Container{_, _, _, _, _, exposure, _, _, _, _, _, _}:
442	      exposure
443	
444	def exposure_of(+k: String, +s: System) -> Exposure:
445	  container_exposure(container(home(k, s), containers(s)))
446	
447	# ---- where it runs ----
448	# On a server, everything is reachable only from the server itself or over the overlay.
449	def private_ok(c: Container, +ns: List<&2, Node>) -> Bool:
450	  match c:
451	    case Container{_, _, _, _, on, +exposure, _, _, _, _, _, _}:
452	      Bool.not(is_server(node_role(on, ns))) || is_tailnet(exposure) || is_local(exposure)
453	
454	def all_private(xs: List<&2, Container>, +ns: List<&2, Node>) -> Bool:
455	  match xs:
456	    case []:
457	      True{}
458	    case c <> rest:
459	      private_ok(c, ns) && all_private(rest, ns)
460	
461	def servers_private(+s: System) -> Bool:
462	  all_private(containers(s), nodes(s))
463	
464	# A device reaches a server over the overlay only when the destination is exposed to the tailnet.
465	def devices_via_network.go(xs: List<&2, Link>, +s: System) -> Bool:
466	  match xs:
467	    case []:
468	      True{}
469	    case l <> rest:
470	      match l:
471	        case Link{src, +dst, _, _}:
472	          (Bool.not(is_device(role_of(src, s)) && is_server(role_of(dst, s))) ||
473	            is_tailnet(exposure_of(dst, s))) && devices_via_network.go(rest, s)
474	
475	def devices_via_network(+s: System) -> Bool:
476	  devices_via_network.go(links(s), s)
477	
478	# A server container needs overlay exposure exactly when a device-origin link reaches it.
479	def device_reaches(+key: String, xs: List<&2, Link>, +s: System) -> Bool:
480	  match xs:
481	    case []:
482	      False{}
483	    case Link{src, dst, _, _} <> rest:
484	      (is_device(role_of(src, s)) && str_eq(home(dst, s), key)) || device_reaches(key, rest, s)
485	
486	def exposure_for_reach(c: Container, reached: Bool) -> Bool:
487	  match reached:
488	    case True{}: is_tailnet(container_exposure(c))
489	    case False{}: is_local(container_exposure(c))
490	
491	def exposure_follows_reach.go(xs: List<&2, Container>, +s: System) -> Bool:
492	  match xs:
493	    case []:
494	      True{}
495	    case +c <> rest:
496	      (Bool.not(is_server(role_of(ckey(c), s))) ||
497	        exposure_for_reach(c, device_reaches(ckey(c), links(s), s))) &&
498	        exposure_follows_reach.go(rest, s)
499	
500	def exposure_follows_reach(+s: System) -> Bool:
501	  exposure_follows_reach.go(containers(s), s)
502	
503	# ---- what it is: minimality, every capability provided exactly once ----
504	def is_cap(want: Cap, c: Cap) -> Bool:
505	  match want c:
506	    case Hosting{} Hosting{}:
507	      True{}
508	    case PrivateHosting{} PrivateHosting{}:
509	      True{}
510	    case Realtime{} Realtime{}:
511	      True{}
512	    case BlobStore{} BlobStore{}:
513	      True{}
514	    case Observability{} Observability{}:
515	      True{}
516	    case _ _:
517	      False{}
518	
519	def count_in(+want: Cap, cs: List<&2, Cap>) -> Nat:
520	  match cs:
521	    case []:
522	      0n
523	    case c <> rest:
524	      Nat.add(one_if(is_cap(want, c)), count_in(want, rest))
525	
526	def direct(+want: Cap, xs: List<&2, Container>) -> Nat:
527	  match xs:
528	    case []:
529	      0n
530	    case c <> rest:
531	      Nat.add(count_in(want, caps(c)), direct(want, rest))
532	
533	def tailnet_hosting.go(xs: List<&2, Container>) -> Nat:
534	  match xs:
535	    case []:
536	      0n
537	    case c <> rest:
538	      match c:
539	        case Container{_, _, _, _, _, exposure, cs, _, _, _, _, _}:
540	          Nat.add(one_if(is_tailnet(exposure) && Nat.is_gt(count_in(Hosting{}, cs), 0n)), tailnet_hosting.go(rest))
541	
542	# How many containers host the app at Tailnet exposure.
543	def tailnet_hosting(+s: System) -> Nat:
544	  tailnet_hosting.go(containers(s))
545	
546	# How many containers provide `want`. One tailnet host plus one overlay composes private hosting.
547	def provided(want: Cap, +s: System) -> Nat:
548	  match want:
549	    case PrivateHosting{}:
550	      Nat.add(direct(PrivateHosting{}, containers(s)), one_if(Nat.is_eq(tailnet_hosting(s), 1n) && Nat.is_eq(overlay_nodes(s), 1n)))
551	    case _:
552	      direct(want, containers(s))
553	
554	# ---- observability: everything we run reports to the observability provider ----
555	def cons_if(b: Bool, k: String, xs: List<&2, String>) -> List<&2, String>:
556	  match b:
557	    case True{}:
558	      k <> xs
559	    case False{}:
560	      xs
561	
562	# Keys of the containers that provide `want`.
563	def providers(+want: Cap, xs: List<&2, Container>) -> List<&2, String>:
564	  match xs:
565	    case []:
566	      []
567	    case +c <> rest:
568	      cons_if(Nat.is_gt(count_in(want, caps(c)), 0n), ckey(c), providers(want, rest))
569	
570	# The container a link end belongs to: a part's container, else the key itself.
571	def part_container(ps: List<&2, Part>, +k: String) -> String:
572	  match ps:
573	    case []:
574	      k
575	    case +p <> rest:
576	      pick_str(str_eq(k, pkey(p)), pin(p), part_container(rest, k))
577	
578	# Some link from container `k` (or one of its parts) reaches one of `obs`.
579	def reports_to(ls: List<&2, Link>, +k: String, +ps: List<&2, Part>, +obs: List<&2, String>) -> Bool:
580	  match ls:
581	    case []:
582	      False{}
583	    case Link{src, dst, _, _} <> rest:
584	      (str_eq(k, part_container(ps, src)) && has(dst, obs)) || reports_to(rest, k, ps, obs)
585	
586	def observed.go(xs: List<&2, Container>, +s: System, +obs: List<&2, String>) -> Bool:
587	  match xs:
588	    case []:
589	      True{}
590	    case c <> rest:
591	      match c:
592	        case Container{+k, _, _, owner, _, _, _, source, _, _, _, _}:
593	          (Bool.not(is_ours(owner) && Bool.not(str_eq(source, ""))) || reports_to(links(s), k, parts(s), obs)) && observed.go(rest, s, obs)
594	
595	# Every container we build (ours, with source) links to a container providing Observability.
596	def observed(+s: System) -> Bool:
597	  observed.go(containers(s), s, providers(Observability{}, containers(s)))
598	
599	def tailnet_data_apis.go(xs: List<&2, Container>) -> Nat:
600	  match xs:
601	    case []:
602	      0n
603	    case c <> rest:
604	      match c:
605	        case Container{_, _, kind, _, _, exposure, _, _, _, _, _, _}:
606	          Nat.add(one_if(is_data_api(kind) && is_tailnet(exposure)), tailnet_data_apis.go(rest))
607	
608	# The data APIs the overlay reaches: the client's data API. Local and outside ones are its sources.
609	def tailnet_data_apis(+s: System) -> Nat:
610	  tailnet_data_apis.go(containers(s))
611	
612	def own_data_apis.go(xs: List<&2, Container>, +ns: List<&2, Node>) -> Nat:
613	  match xs:
614	    case []:
615	      0n
616	    case c <> rest:
617	      match c:
618	        case Container{_, _, kind, _, on, _, _, _, _, _, _, _}:
619	          Nat.add(one_if(is_data_api(kind) && Bool.not(is_outside(node_role(on, ns)))), own_data_apis.go(rest, ns))
620	
621	# The system's own data APIs: those not on someone else's servers. "Exactly one" means one store.
622	def own_data_apis(+s: System) -> Nat:
623	  own_data_apis.go(containers(s), nodes(s))
624	
625	# A data API may also host the app only while it is private.
626	def shared_hosting_ok(c: Container) -> Bool:
627	  match c:
628	    case Container{_, _, kind, _, _, +exposure, +cs, _, _, _, _, _}:
629	      Bool.not(Nat.is_gt(count_in(Hosting{}, cs), 0n) && is_data_api(kind)) || is_tailnet(exposure) || is_local(exposure)
630	
631	def shared_hosting_private.go(xs: List<&2, Container>) -> Bool:
632	  match xs:
633	    case []:
634	      True{}
635	    case c <> rest:
636	      shared_hosting_ok(c) && shared_hosting_private.go(rest)
637	
638	def shared_hosting_private(+s: System) -> Bool:
639	  shared_hosting_private.go(containers(s))
640	
641	# ---- a goal: every part of our own non-client containers is Rust ----
642	def backend(c: Container) -> Bool:
643	  match c:
644	    case Container{_, _, kind, owner, _, _, _, _, _, _, _, _}:
645	      is_ours(owner) && Bool.not(is_client(kind))
646	
647	def rust_ok(p: Part, +s: System) -> Bool:
648	  match p:
649	    case Part{_, _, lang, i, _}:
650	      Bool.not(backend(container(i, containers(s)))) || is_rust(lang)
651	
652	def all_rust.go(xs: List<&2, Part>, +s: System) -> Bool:
653	  match xs:
654	    case []:
655	      True{}
656	    case p <> rest:
657	      rust_ok(p, s) && all_rust.go(rest, s)
658	
659	def all_rust(+s: System) -> Bool:
660	  all_rust.go(parts(s), s)
661	
662	# Every modeled part belongs to a container we build; someone else's program is a black box.
663	def container_ours(c: Container) -> Bool:
664	  match c:
665	    case Container{_, _, _, owner, _, _, _, _, _, _, _, _}:
666	      is_ours(owner)
667	
668	def parts_ours.go(xs: List<&2, Part>, +s: System) -> Bool:
669	  match xs:
670	    case []:
671	      True{}
672	    case p <> rest:
673	      container_ours(container(pin(p), containers(s))) && parts_ours.go(rest, s)
674	
675	def parts_ours(+s: System) -> Bool:
676	  parts_ours.go(parts(s), s)
677	
678	# ---- the diagram (D2): nodes as boxes, containers inside their node, parts inside their container ----
679	def path(+k: String, +s: System) -> String:
680	  node_of(k, s) ++ "." ++ pick_str(String.eq(home(k, s), k), k, home(k, s) ++ "." ++ k)
681	
682	def node_box(n: Node) -> String:
683	  match n:
684	    case Node{k, name, role, _}:
685	      match role:
686	        case Outside{}:
687	          k ++ ": \"" ++ name ++ "\" {class: node; style.stroke-dash: 4; style.fill: \"#FFFFFF\"}\n"
688	        case _:
689	          k ++ ": \"" ++ name ++ "\" {class: node}\n"
690	
691	def node_boxes(xs: List<&2, Node>) -> String:
692	  match xs:
693	    case []:
694	      ""
695	    case n <> rest:
696	      node_box(n) ++ node_boxes(rest)
697	
698	def stack_label(frameworks: List<&2, String>, libraries: List<&2, String>) -> String:
699	  match frameworks:
700	    case []:
701	      match libraries:
702	        case []:
703	          ""
704	        case _:
705	          "\\n[" ++ String.join(libraries, ", ") ++ "]"
706	    case _:
707	      match libraries:
708	        case []:
709	          "\\n[" ++ String.join(frameworks, ", ") ++ "]"
710	        case _:
711	          "\\n[" ++ String.join(frameworks, ", ") ++ " · " ++ String.join(libraries, ", ") ++ "]"
712	
713	def container_box(c: Container) -> String:
714	  match c:
715	    case Container{k, name, _, _, on, _, _, _, _, frameworks, libraries, _}:
716	      on ++ "." ++ k ++ ": \"" ++ name ++ stack_label(frameworks, libraries) ++ "\" {class: container}\n"
717	
718	def container_boxes(xs: List<&2, Container>) -> String:
719	  match xs:
720	    case []:
721	      ""
722	    case c <> rest:
723	      container_box(c) ++ container_boxes(rest)
724	
725	def part_box(p: Part, +s: System) -> String:
726	  match p:
727	    case Part{+k, name, _, _, _}:
728	      path(k, s) ++ ": \"" ++ name ++ "\" {class: part}\n"
729	
730	def part_boxes(xs: List<&2, Part>, +s: System) -> String:
731	  match xs:
732	    case []:
733	      ""
734	    case p <> rest:
735	      part_box(p, s) ++ part_boxes(rest, s)
736	
737	def style(live: Bool) -> String:
738	  match live:
739	    case True{}:
740	      "live"
741	    case False{}:
742	      "plain"
743	
744	def edges(xs: List<&2, Link>, +s: System) -> String:
745	  match xs:
746	    case []:
747	      ""
748	    case l <> rest:
749	      match l:
750	        case Link{src, dst, label, live}:
751	          path(src, s) ++ " -> " ++ path(dst, s) ++ ": \"" ++ label ++ "\" {class: " ++ style(live) ++ "}\n" ++ edges(rest, s)
752	
753	def d2(+s: System) -> String:
754	  "direction: right\n" ++
755	  "classes: {\n" ++
756	  "  node: {style: {fill: \"#F2F2F2\"; stroke: \"#D9D9D9\"; border-radius: 14; font-size: 26; bold: true}}\n" ++
757	  "  container: {style: {fill: \"#FFFFFF\"; stroke: \"#8C8C8C\"; border-radius: 10; font-size: 22}}\n" ++
758	  "  part: {style: {fill: \"#FAFAFA\"; stroke: \"#BFBFBF\"; border-radius: 8; font-size: 18}}\n" ++
759	  "  live: {style: {stroke: \"#3E8A62\"; stroke-width: 3; font-color: \"#3E8A62\"; font-size: 18; bold: true}}\n" ++
760	  "  plain: {style: {stroke: \"#8C8C8C\"; stroke-width: 2; font-color: \"#8C8C8C\"; font-size: 16}}\n" ++
761	  "}\n" ++
762	  node_boxes(nodes(s)) ++ container_boxes(containers(s)) ++ part_boxes(parts(s), s) ++ edges(links(s), s)