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