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