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