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