arc.bend
near-architecture@0.2.0.0 · 524 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_device(r: NodeRole) -> Bool:
164 match r:
165 case UserDevice{}:
166 True{}
167 case _:
168 False{}
169
170def is_client(k: ContainerKind) -> Bool:
171 match k:
172 case Client{}:
173 True{}
174 case _:
175 False{}
176
177def is_data_api(k: ContainerKind) -> Bool:
178 match k:
179 case DataApi{}:
180 True{}
181 case _:
182 False{}
183
184def is_ours(o: Owner) -> Bool:
185 match o:
186 case Ours{}:
187 True{}
188 case Theirs{}:
189 False{}
190
191def is_local(e: Exposure) -> Bool:
192 match e:
193 case Local{}:
194 True{}
195 case _:
196 False{}
197
198def is_tailnet(e: Exposure) -> Bool:
199 match e:
200 case Tailnet{}:
201 True{}
202 case _:
203 False{}
204
205def is_rust(l: Lang) -> Bool:
206 match l:
207 case Rust{}:
208 True{}
209 case _:
210 False{}
211
212# ---- keys, like foreign keys ----
213def str_eq(a: String, b: String) -> Bool:
214 String.eq(a, b)
215
216def has(+s: String, xs: List<&2, String>) -> Bool:
217 match xs:
218 case []:
219 False{}
220 case x <> rest:
221 str_eq(s, x) || has(s, rest)
222
223def pick_str(c: Bool, a: String, b: String) -> String:
224 match c:
225 case True{}:
226 a
227 case False{}:
228 b
229
230# No key names two things.
231def distinct_keys(xs: List<&2, String>) -> Bool:
232 match xs:
233 case []:
234 True{}
235 case +k <> +rest:
236 Bool.not(has(k, rest)) && distinct_keys(rest)
237
238# Every key in `xs` names something in `ks`.
239def all_in(xs: List<&2, String>, +ks: List<&2, String>) -> Bool:
240 match xs:
241 case []:
242 True{}
243 case x <> rest:
244 has(x, ks) && all_in(rest, ks)
245
246def part_ins(xs: List<&2, Part>) -> List<&2, String>:
247 match xs:
248 case []:
249 []
250 case p <> rest:
251 pin(p) <> part_ins(rest)
252
253def container_ons(xs: List<&2, Container>) -> List<&2, String>:
254 match xs:
255 case []:
256 []
257 case c <> rest:
258 con(c) <> container_ons(rest)
259
260def link_ends(xs: List<&2, Link>) -> List<&2, String>:
261 match xs:
262 case []:
263 []
264 case l <> rest:
265 match l:
266 case Link{a, b, _, _}:
267 a <> b <> link_ends(rest)
268
269# The system is well formed: node keys and container/part keys are unique, every container is on
270# a node, every part in a container, and every link joins two things that exist.
271def well_formed(+s: System) -> Bool:
272 distinct_keys(nkeys(nodes(s))) && distinct_keys(keys(s)) &&
273 all_in(container_ons(containers(s)), nkeys(nodes(s))) &&
274 all_in(part_ins(parts(s)), ckeys(containers(s))) &&
275 all_in(link_ends(links(s)), keys(s))
276
277# ---- looking things up ----
278def part_home(+k: String, xs: List<&2, Part>) -> String:
279 match xs:
280 case []:
281 ""
282 case +p <> rest:
283 pick_str(str_eq(k, pkey(p)), pin(p), part_home(k, rest))
284
285# The container a key belongs to: itself, or the one its part sits in.
286def home(+k: String, +s: System) -> String:
287 pick_str(has(k, ckeys(containers(s))), k, part_home(k, parts(s)))
288
289def none() -> Container:
290 Container{"", "", Worker{}, Theirs{}, "", Public{}, []}
291
292def pick_c(hit: Bool, c: Container, other: Container) -> Container:
293 match hit:
294 case True{}:
295 c
296 case False{}:
297 other
298
299# The container with key `k` (an empty one when `k` is unknown; well_formed rules that out).
300def container(+k: String, xs: List<&2, Container>) -> Container:
301 match xs:
302 case []:
303 none()
304 case +c <> rest:
305 pick_c(str_eq(k, ckey(c)), c, container(k, rest))
306
307def pick_r(hit: Bool, r: NodeRole, other: NodeRole) -> NodeRole:
308 match hit:
309 case True{}:
310 r
311 case False{}:
312 other
313
314def node_role(+k: String, xs: List<&2, Node>) -> NodeRole:
315 match xs:
316 case []:
317 Outside{}
318 case n <> rest:
319 match n:
320 case Node{nk, _, r}:
321 pick_r(str_eq(k, nk), r, node_role(k, rest))
322
323# The node a container or part runs on, and its role.
324def node_of(+k: String, +s: System) -> String:
325 con(container(home(k, s), containers(s)))
326
327def role_of(+k: String, +s: System) -> NodeRole:
328 node_role(node_of(k, s), nodes(s))
329
330# ---- where it runs ----
331# On a server, everything is reachable only from the server itself or over the private network.
332def private_ok(c: Container, +ns: List<&2, Node>) -> Bool:
333 match c:
334 case Container{_, _, _, _, on, +exposure, _}:
335 Bool.not(is_server(node_role(on, ns))) || is_tailnet(exposure) || is_local(exposure)
336
337def all_private(xs: List<&2, Container>, +ns: List<&2, Node>) -> Bool:
338 match xs:
339 case []:
340 True{}
341 case c <> rest:
342 private_ok(c, ns) && all_private(rest, ns)
343
344def servers_private(+s: System) -> Bool:
345 all_private(containers(s), nodes(s))
346
347# A device reaches a server only through the private network: no link goes straight from one to the other.
348def devices_via_network.go(xs: List<&2, Link>, +s: System) -> Bool:
349 match xs:
350 case []:
351 True{}
352 case l <> rest:
353 match l:
354 case Link{src, dst, _, _}:
355 Bool.not(is_device(role_of(src, s)) && is_server(role_of(dst, s))) && devices_via_network.go(rest, s)
356
357def devices_via_network(+s: System) -> Bool:
358 devices_via_network.go(links(s), s)
359
360# ---- what it is: minimality, every capability provided exactly once ----
361def is_cap(want: Cap, c: Cap) -> Bool:
362 match want c:
363 case Hosting{} Hosting{}:
364 True{}
365 case PrivateAccess{} PrivateAccess{}:
366 True{}
367 case PrivateHosting{} PrivateHosting{}:
368 True{}
369 case Realtime{} Realtime{}:
370 True{}
371 case BlobStore{} BlobStore{}:
372 True{}
373 case _ _:
374 False{}
375
376def one_if(b: Bool) -> Nat:
377 match b:
378 case True{}:
379 1n
380 case False{}:
381 0n
382
383def count_in(+want: Cap, cs: List<&2, Cap>) -> Nat:
384 match cs:
385 case []:
386 0n
387 case c <> rest:
388 Nat.add(one_if(is_cap(want, c)), count_in(want, rest))
389
390def direct(+want: Cap, xs: List<&2, Container>) -> Nat:
391 match xs:
392 case []:
393 0n
394 case c <> rest:
395 Nat.add(count_in(want, caps(c)), direct(want, rest))
396
397# How many containers provide `want`. Hosting plus private access compose into private hosting.
398def provided(want: Cap, +s: System) -> Nat:
399 match want:
400 case PrivateHosting{}:
401 Nat.add(direct(PrivateHosting{}, containers(s)), one_if(Nat.is_eq(direct(Hosting{}, containers(s)), 1n) && Nat.is_eq(direct(PrivateAccess{}, containers(s)), 1n)))
402 case _:
403 direct(want, containers(s))
404
405def tailnet_data_apis.go(xs: List<&2, Container>) -> Nat:
406 match xs:
407 case []:
408 0n
409 case c <> rest:
410 match c:
411 case Container{_, _, kind, _, _, exposure, _}:
412 Nat.add(one_if(is_data_api(kind) && is_tailnet(exposure)), tailnet_data_apis.go(rest))
413
414# The data APIs the private network reaches: the client's data API. Local and outside ones are its sources.
415def tailnet_data_apis(+s: System) -> Nat:
416 tailnet_data_apis.go(containers(s))
417
418# A data API may also host the app only while it is private.
419def shared_hosting_ok(c: Container) -> Bool:
420 match c:
421 case Container{_, _, kind, _, _, +exposure, +cs}:
422 Bool.not(Nat.is_gt(count_in(Hosting{}, cs), 0n) && is_data_api(kind)) || is_tailnet(exposure) || is_local(exposure)
423
424def shared_hosting_private.go(xs: List<&2, Container>) -> Bool:
425 match xs:
426 case []:
427 True{}
428 case c <> rest:
429 shared_hosting_ok(c) && shared_hosting_private.go(rest)
430
431def shared_hosting_private(+s: System) -> Bool:
432 shared_hosting_private.go(containers(s))
433
434# ---- a goal: every part of our own non-client containers is Rust ----
435def backend(c: Container) -> Bool:
436 match c:
437 case Container{_, _, kind, owner, _, _, _}:
438 is_ours(owner) && Bool.not(is_client(kind))
439
440def rust_ok(p: Part, +s: System) -> Bool:
441 match p:
442 case Part{_, _, lang, i}:
443 Bool.not(backend(container(i, containers(s)))) || is_rust(lang)
444
445def all_rust.go(xs: List<&2, Part>, +s: System) -> Bool:
446 match xs:
447 case []:
448 True{}
449 case p <> rest:
450 rust_ok(p, s) && all_rust.go(rest, s)
451
452def all_rust(+s: System) -> Bool:
453 all_rust.go(parts(s), s)
454
455# ---- the diagram (D2): nodes as boxes, containers inside their node, parts inside their container ----
456def path(+k: String, +s: System) -> String:
457 node_of(k, s) ++ "." ++ pick_str(String.eq(home(k, s), k), k, home(k, s) ++ "." ++ k)
458
459def node_box(n: Node) -> String:
460 match n:
461 case Node{k, name, role}:
462 match role:
463 case Outside{}:
464 k ++ ": \"" ++ name ++ "\" {class: node; style.stroke-dash: 4; style.fill: \"#FFFFFF\"}\n"
465 case _:
466 k ++ ": \"" ++ name ++ "\" {class: node}\n"
467
468def node_boxes(xs: List<&2, Node>) -> String:
469 match xs:
470 case []:
471 ""
472 case n <> rest:
473 node_box(n) ++ node_boxes(rest)
474
475def container_box(c: Container) -> String:
476 match c:
477 case Container{k, name, _, _, on, _, _}:
478 on ++ "." ++ k ++ ": \"" ++ name ++ "\" {class: container}\n"
479
480def container_boxes(xs: List<&2, Container>) -> String:
481 match xs:
482 case []:
483 ""
484 case c <> rest:
485 container_box(c) ++ container_boxes(rest)
486
487def part_box(p: Part, +s: System) -> String:
488 match p:
489 case Part{+k, name, _, _}:
490 path(k, s) ++ ": \"" ++ name ++ "\" {class: part}\n"
491
492def part_boxes(xs: List<&2, Part>, +s: System) -> String:
493 match xs:
494 case []:
495 ""
496 case p <> rest:
497 part_box(p, s) ++ part_boxes(rest, s)
498
499def style(live: Bool) -> String:
500 match live:
501 case True{}:
502 "live"
503 case False{}:
504 "plain"
505
506def edges(xs: List<&2, Link>, +s: System) -> String:
507 match xs:
508 case []:
509 ""
510 case l <> rest:
511 match l:
512 case Link{src, dst, label, live}:
513 path(src, s) ++ " -> " ++ path(dst, s) ++ ": \"" ++ label ++ "\" {class: " ++ style(live) ++ "}\n" ++ edges(rest, s)
514
515def d2(+s: System) -> String:
516 "direction: right\n" ++
517 "classes: {\n" ++
518 " node: {style: {fill: \"#F2F2F2\"; stroke: \"#D9D9D9\"; border-radius: 14; font-size: 26; bold: true}}\n" ++
519 " container: {style: {fill: \"#FFFFFF\"; stroke: \"#8C8C8C\"; border-radius: 10; font-size: 22}}\n" ++
520 " part: {style: {fill: \"#FAFAFA\"; stroke: \"#BFBFBF\"; border-radius: 8; font-size: 18}}\n" ++
521 " live: {style: {stroke: \"#3E8A62\"; stroke-width: 3; font-color: \"#3E8A62\"; font-size: 18; bold: true}}\n" ++
522 " plain: {style: {stroke: \"#8C8C8C\"; stroke-width: 2; font-color: \"#8C8C8C\"; font-size: 16}}\n" ++
523 "}\n" ++
524 node_boxes(nodes(s)) ++ container_boxes(containers(s)) ++ part_boxes(parts(s), s) ++ edges(links(s), s)