arc.bend
near-architecture@0.9.0.0 · 831 lines · 0 definitions
1import 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.
13type NodeRole is Data:
14 UserDevice{}
15 Server{}
16 Overlay{}
17 Outside{}
18
19type PhysicalDevice is Data:
20 PhysicalDevice{key: String, name: String, platform: String}
21
22type Vendor is Data:
23 Vendor{name: String, cloud: String}
24
25type 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.
31type Person is Data:
32 Person{key: String, identity: String}
33type Grant is Data:
34 Grant{person: String, scope: String, actions: List<&2, String>}
35type Budget is Data:
36 Budget{person: String, what: String, amount: Nat, unit: String}
37type Agreement is Data:
38 Agreement{domain: String, people: List<&2, Person>, grants: List<&2, Grant>, budgets: List<&2, Budget>}
39type Host is Data:
40 Owned{device: String}
41 Cloud{provider: String}
42 Other{}
43
44type 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.
54type 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.
64type 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.
69type 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.
79type Cap is Data:
80 Hosting{}
81 PrivateHosting{}
82 Realtime{}
83 BlobStore{}
84 Observability{}
85
86type Lang is Data:
87 Bend{}
88 C{}
89 Rust{}
90 TypeScript{}
91 JavaScript{}
92 Python{}
93 Opaque{}
94
95type 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
98type 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.
102type Link is Data:
103 Link{src: String, dst: String, label: String, live: Bool}
104
105type 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 ----
109def org(s: System) -> Org:
110 match s:
111 case System{o, _, _, _, _}:
112 o
113
114def nodes(s: System) -> List<&2, Node>:
115 match s:
116 case System{_, n, _, _, _}:
117 n
118
119def containers(s: System) -> List<&2, Container>:
120 match s:
121 case System{_, _, c, _, _}:
122 c
123
124def parts(s: System) -> List<&2, Part>:
125 match s:
126 case System{_, _, _, p, _}:
127 p
128
129def links(s: System) -> List<&2, Link>:
130 match s:
131 case System{_, _, _, _, l}:
132 l
133
134def nkey(n: Node) -> String:
135 match n:
136 case Node{k, _, _, _}:
137 k
138
139def ckey(c: Container) -> String:
140 match c:
141 case Container{k, _, _, _, _, _, _, _, _, _, _, _}:
142 k
143
144def con(c: Container) -> String:
145 match c:
146 case Container{_, _, _, _, o, _, _, _, _, _, _, _}:
147 o
148
149def caps(c: Container) -> List<&2, Cap>:
150 match c:
151 case Container{_, _, _, _, _, _, cs, _, _, _, _, _}:
152 cs
153
154def pkey(p: Part) -> String:
155 match p:
156 case Part{k, _, _, _, _}:
157 k
158
159def pin(p: Part) -> String:
160 match p:
161 case Part{_, _, _, i, _}:
162 i
163
164def pon(p: Part) -> String:
165 match p:
166 case Part{_, _, _, _, on}:
167 on
168
169def nkeys(xs: List<&2, Node>) -> List<&2, String>:
170 match xs:
171 case []:
172 []
173 case n <> rest:
174 nkey(n) <> nkeys(rest)
175
176def ckeys(xs: List<&2, Container>) -> List<&2, String>:
177 match xs:
178 case []:
179 []
180 case c <> rest:
181 ckey(c) <> ckeys(rest)
182
183def 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.
191def keys(+s: System) -> List<&2, String>:
192 List.append(&2, String, ckeys(containers(s)), pkeys(parts(s)))
193
194# ---- predicates on the vocabulary ----
195def is_server(r: NodeRole) -> Bool:
196 match r:
197 case Server{}:
198 True{}
199 case _:
200 False{}
201
202def is_outside(r: NodeRole) -> Bool:
203 match r:
204 case Outside{}:
205 True{}
206 case _:
207 False{}
208
209def is_device(r: NodeRole) -> Bool:
210 match r:
211 case UserDevice{}:
212 True{}
213 case _:
214 False{}
215
216def is_overlay(r: NodeRole) -> Bool:
217 match r:
218 case Overlay{}:
219 True{}
220 case _:
221 False{}
222
223def one_if(b: Bool) -> Nat:
224 match b:
225 case True{}:
226 1n
227 case False{}:
228 0n
229
230def 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.
240def overlay_nodes(+s: System) -> Nat:
241 overlay_nodes.go(nodes(s))
242
243def is_client(k: ContainerKind) -> Bool:
244 match k:
245 case Client{}:
246 True{}
247 case _:
248 False{}
249
250def is_data_api(k: ContainerKind) -> Bool:
251 match k:
252 case DataApi{}:
253 True{}
254 case _:
255 False{}
256
257def is_ours(o: Owner) -> Bool:
258 match o:
259 case Ours{}:
260 True{}
261 case Theirs{}:
262 False{}
263
264def is_local(e: Exposure) -> Bool:
265 match e:
266 case Local{}:
267 True{}
268 case _:
269 False{}
270
271def is_tailnet(e: Exposure) -> Bool:
272 match e:
273 case Tailnet{}:
274 True{}
275 case _:
276 False{}
277
278def is_rust(l: Lang) -> Bool:
279 match l:
280 case Rust{}:
281 True{}
282 case _:
283 False{}
284
285# ---- keys, like foreign keys ----
286def str_eq(a: String, b: String) -> Bool:
287 String.eq(a, b)
288
289def 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
296def 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
303def 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
312def 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
317def 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.
325def owned_nodes(+s: System) -> Bool:
326 owned_nodes.go(nodes(s), org(s))
327
328def 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.
336def 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`.
344def 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
351def 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
358def 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
365def 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
372def 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.
383def 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 ----
391def 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.
399def home(+k: String, +s: System) -> String:
400 pick_str(has(k, ckeys(containers(s))), k, part_home(k, parts(s)))
401
402def none() -> Container:
403 Container{"", "", Worker{}, Theirs{}, "", Public{}, [], "", [], [], [], []}
404
405def 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).
413def 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
420def pick_r(hit: Bool, r: NodeRole, other: NodeRole) -> NodeRole:
421 match hit:
422 case True{}:
423 r
424 case False{}:
425 other
426
427def 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
436def 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.
444def 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
447def role_of(+k: String, +s: System) -> NodeRole:
448 node_role(node_of(k, s), nodes(s))
449
450def container_exposure(c: Container) -> Exposure:
451 match c:
452 case Container{_, _, _, _, _, exposure, _, _, _, _, _, _}:
453 exposure
454
455def 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.
460def 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
465def 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
472def 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.
476def 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
486def 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.
490def 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
497def 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
502def 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
511def 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 ----
515def 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
530def 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
537def 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
544def 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.
554def 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.
558def 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 ----
566def 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`.
574def 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.
582def 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`.
590def 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
597def 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.
607def observed(+s: System) -> Bool:
608 observed.go(containers(s), s, providers(Observability{}, containers(s)))
609
610def 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.
620def tailnet_data_apis(+s: System) -> Nat:
621 tailnet_data_apis.go(containers(s))
622
623def 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.
633def 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.
637def 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
642def 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
649def 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 ----
653def backend(c: Container) -> Bool:
654 match c:
655 case Container{_, _, kind, owner, _, _, _, _, _, _, _, _}:
656 is_ours(owner) && Bool.not(is_client(kind))
657
658def 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
663def 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
670def 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.
674def container_ours(c: Container) -> Bool:
675 match c:
676 case Container{_, _, _, owner, _, _, _, _, _, _, _, _}:
677 is_ours(owner)
678
679def 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
686def 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 ----
690def 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
693def 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
702def 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
709def 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
724def 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
729def 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
736def part_box(p: Part, +s: System) -> String:
737 match p:
738 case Part{+k, name, _, _, _}:
739 path(k, s) ++ ": \"" ++ name ++ "\" {class: part}\n"
740
741def 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
748def style(live: Bool) -> String:
749 match live:
750 case True{}:
751 "live"
752 case False{}:
753 "plain"
754
755def 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
764def 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 ----
776def ends_with_at(+identity: String, +domain: String) -> Bool:
777 String.ends_with(String.to_lower(identity), "@" ++ String.to_lower(domain))
778
779def 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.
787def people_in_domain(a: Agreement) -> Bool:
788 match a:
789 case Agreement{domain, people, _, _}:
790 people_in.go(people, domain)
791
792def 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
799def 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.
807def identities_known(ids: List<&2, String>, a: Agreement) -> Bool:
808 match a:
809 case Agreement{_, people, _, _}:
810 identities_known.go(ids, people)
811
812def 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
819def 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.
827def granted(a: Agreement, +person: String, +scope: String) -> List<&2, String>:
828 match a:
829 case Agreement{_, _, grants, _}:
830 granted.go(grants, person, scope)
831