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