arc.bend

near-architecture@0.9.1.0 · 833 lines · 130 definitions

1import 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.
15type NodeRole is Data:
16  UserDevice{}
17  Server{}
18  Overlay{}
19  Outside{}
20
21type PhysicalDevice is Data:
22  PhysicalDevice{key: String, name: String, platform: String}
23
24type Vendor is Data:
25  Vendor{name: String, cloud: String}
26
27type 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.
33type Person is Data:
34  Person{key: String, identity: String}
35type Grant is Data:
36  Grant{person: String, scope: String, actions: List<&2, String>}
37type Budget is Data:
38  Budget{person: String, what: String, amount: Nat, unit: String}
39type Agreement is Data:
40  Agreement{domain: String, people: List<&2, Person>, grants: List<&2, Grant>, budgets: List<&2, Budget>}
41type Host is Data:
42  Owned{device: String}
43  Cloud{provider: String}
44  Other{}
45
46type 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.
56type 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.
66type 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.
71type 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.
81type Cap is Data:
82  Hosting{}
83  PrivateHosting{}
84  Realtime{}
85  BlobStore{}
86  Observability{}
87
88type Lang is Data:
89  Bend{}
90  C{}
91  Rust{}
92  TypeScript{}
93  JavaScript{}
94  Python{}
95  Opaque{}
96
97type 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
100type 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.
104type Link is Data:
105  Link{src: String, dst: String, label: String, live: Bool}
106
107type 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 ----
111def org(s: System) -> Org:
112  match s:
113    case System{o, _, _, _, _}:
114      o
115
116def nodes(s: System) -> List<&2, Node>:
117  match s:
118    case System{_, n, _, _, _}:
119      n
120
121def containers(s: System) -> List<&2, Container>:
122  match s:
123    case System{_, _, c, _, _}:
124      c
125
126def parts(s: System) -> List<&2, Part>:
127  match s:
128    case System{_, _, _, p, _}:
129      p
130
131def links(s: System) -> List<&2, Link>:
132  match s:
133    case System{_, _, _, _, l}:
134      l
135
136def nkey(n: Node) -> String:
137  match n:
138    case Node{k, _, _, _}:
139      k
140
141def ckey(c: Container) -> String:
142  match c:
143    case Container{k, _, _, _, _, _, _, _, _, _, _, _}:
144      k
145
146def con(c: Container) -> String:
147  match c:
148    case Container{_, _, _, _, o, _, _, _, _, _, _, _}:
149      o
150
151def caps(c: Container) -> List<&2, Cap>:
152  match c:
153    case Container{_, _, _, _, _, _, cs, _, _, _, _, _}:
154      cs
155
156def pkey(p: Part) -> String:
157  match p:
158    case Part{k, _, _, _, _}:
159      k
160
161def pin(p: Part) -> String:
162  match p:
163    case Part{_, _, _, i, _}:
164      i
165
166def pon(p: Part) -> String:
167  match p:
168    case Part{_, _, _, _, on}:
169      on
170
171def nkeys(xs: List<&2, Node>) -> List<&2, String>:
172  match xs:
173    case []:
174      []
175    case n <> rest:
176      nkey(n) <> nkeys(rest)
177
178def ckeys(xs: List<&2, Container>) -> List<&2, String>:
179  match xs:
180    case []:
181      []
182    case c <> rest:
183      ckey(c) <> ckeys(rest)
184
185def 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.
193def keys(+s: System) -> List<&2, String>:
194  List.append(&2, String, ckeys(containers(s)), pkeys(parts(s)))
195
196# ---- predicates on the vocabulary ----
197def is_server(r: NodeRole) -> Bool:
198  match r:
199    case Server{}:
200      True{}
201    case _:
202      False{}
203
204def is_outside(r: NodeRole) -> Bool:
205  match r:
206    case Outside{}:
207      True{}
208    case _:
209      False{}
210
211def is_device(r: NodeRole) -> Bool:
212  match r:
213    case UserDevice{}:
214      True{}
215    case _:
216      False{}
217
218def is_overlay(r: NodeRole) -> Bool:
219  match r:
220    case Overlay{}:
221      True{}
222    case _:
223      False{}
224
225def one_if(b: Bool) -> Nat:
226  match b:
227    case True{}:
228      1n
229    case False{}:
230      0n
231
232def 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.
242def overlay_nodes(+s: System) -> Nat:
243  overlay_nodes.go(nodes(s))
244
245def is_client(k: ContainerKind) -> Bool:
246  match k:
247    case Client{}:
248      True{}
249    case _:
250      False{}
251
252def is_data_api(k: ContainerKind) -> Bool:
253  match k:
254    case DataApi{}:
255      True{}
256    case _:
257      False{}
258
259def is_ours(o: Owner) -> Bool:
260  match o:
261    case Ours{}:
262      True{}
263    case Theirs{}:
264      False{}
265
266def is_local(e: Exposure) -> Bool:
267  match e:
268    case Local{}:
269      True{}
270    case _:
271      False{}
272
273def is_tailnet(e: Exposure) -> Bool:
274  match e:
275    case Tailnet{}:
276      True{}
277    case _:
278      False{}
279
280def is_rust(l: Lang) -> Bool:
281  match l:
282    case Rust{}:
283      True{}
284    case _:
285      False{}
286
287# ---- keys, like foreign keys ----
288def str_eq(a: String, b: String) -> Bool:
289  String.eq(a, b)
290
291def 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
298def 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
305def 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
314def 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
319def 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.
327def owned_nodes(+s: System) -> Bool:
328  owned_nodes.go(nodes(s), org(s))
329
330def 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.
338def 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`.
346def 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
353def 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
360def 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
367def 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
374def 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.
385def 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 ----
393def 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.
401def home(+k: String, +s: System) -> String:
402  pick_str(has(k, ckeys(containers(s))), k, part_home(k, parts(s)))
403
404def none() -> Container:
405  Container{"", "", Worker{}, Theirs{}, "", Public{}, [], "", [], [], [], []}
406
407def 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).
415def 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
422def pick_r(hit: Bool, r: NodeRole, other: NodeRole) -> NodeRole:
423  match hit:
424    case True{}:
425      r
426    case False{}:
427      other
428
429def 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
438def 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.
446def 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
449def role_of(+k: String, +s: System) -> NodeRole:
450  node_role(node_of(k, s), nodes(s))
451
452def container_exposure(c: Container) -> Exposure:
453  match c:
454    case Container{_, _, _, _, _, exposure, _, _, _, _, _, _}:
455      exposure
456
457def 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.
462def 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
467def 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
474def 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.
478def 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
488def 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.
492def 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
499def 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
504def 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
513def 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 ----
517def 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
532def 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
539def 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
546def 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.
556def 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.
560def 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 ----
568def 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`.
576def 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.
584def 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`.
592def 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
599def 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.
609def observed(+s: System) -> Bool:
610  observed.go(containers(s), s, providers(Observability{}, containers(s)))
611
612def 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.
622def tailnet_data_apis(+s: System) -> Nat:
623  tailnet_data_apis.go(containers(s))
624
625def 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.
635def 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.
639def 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
644def 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
651def 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 ----
655def backend(c: Container) -> Bool:
656  match c:
657    case Container{_, _, kind, owner, _, _, _, _, _, _, _, _}:
658      is_ours(owner) && Bool.not(is_client(kind))
659
660def 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
665def 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
672def 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.
676def container_ours(c: Container) -> Bool:
677  match c:
678    case Container{_, _, _, owner, _, _, _, _, _, _, _, _}:
679      is_ours(owner)
680
681def 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
688def 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 ----
692def 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
695def 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
704def 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
711def 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
726def 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
731def 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
738def part_box(p: Part, +s: System) -> String:
739  match p:
740    case Part{+k, name, _, _, _}:
741      path(k, s) ++ ": \"" ++ name ++ "\" {class: part}\n"
742
743def 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
750def style(live: Bool) -> String:
751  match live:
752    case True{}:
753      "live"
754    case False{}:
755      "plain"
756
757def 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
766def 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 ----
778def ends_with_at(+identity: String, +domain: String) -> Bool:
779  String.ends_with(String.to_lower(identity), "@" ++ String.to_lower(domain))
780
781def 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.
789def people_in_domain(a: Agreement) -> Bool:
790  match a:
791    case Agreement{domain, people, _, _}:
792      people_in.go(people, domain)
793
794def 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
801def 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.
809def identities_known(ids: List<&2, String>, a: Agreement) -> Bool:
810  match a:
811    case Agreement{_, people, _, _}:
812      identities_known.go(ids, people)
813
814def 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
821def 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.
829def granted(a: Agreement, +person: String, +scope: String) -> List<&2, String>:
830  match a:
831    case Agreement{_, _, grants, _}:
832      granted.go(grants, person, scope)
833