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