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