1	import 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.
12	type NodeRole is Data:
13	  UserDevice{}
14	  Server{}
15	  Overlay{}
16	  Outside{}
17	
18	type 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. AgentsApi: runs agent threads (the harness an app drives).
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.
26	type ContainerKind is Data:
27	  Client{}
28	  Network{}
29	  DataApi{}
30	  AgentsApi{}
31	  ModelApi{}
32	  Cli{}
33	  Worker{}
34	
35	# Whether the project builds and runs it, or uses it as it is.
36	type 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.
41	type 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).
50	type Cap is Data:
51	  Hosting{}
52	  PrivateAccess{}
53	  PrivateHosting{}
54	  Realtime{}
55	  BlobStore{}
56	
57	type Lang is Data:
58	  Bend{}
59	  C{}
60	  Rust{}
61	  TypeScript{}
62	  JavaScript{}
63	  Python{}
64	  Opaque{}
65	
66	type Container is Data:
67	  Container{key: String, name: String, kind: ContainerKind, owner: Owner, on: String, exposure: Exposure, caps: List<&2, Cap>}
68	
69	type 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.
73	type Link is Data:
74	  Link{src: String, dst: String, label: String, live: Bool}
75	
76	type System is Data:
77	  System{nodes: List<&2, Node>, containers: List<&2, Container>, parts: List<&2, Part>, links: List<&2, Link>}
78	
79	# ---- access ----
80	def nodes(s: System) -> List<&2, Node>:
81	  match s:
82	    case System{n, _, _, _}:
83	      n
84	
85	def containers(s: System) -> List<&2, Container>:
86	  match s:
87	    case System{_, c, _, _}:
88	      c
89	
90	def parts(s: System) -> List<&2, Part>:
91	  match s:
92	    case System{_, _, p, _}:
93	      p
94	
95	def links(s: System) -> List<&2, Link>:
96	  match s:
97	    case System{_, _, _, l}:
98	      l
99	
100	def nkey(n: Node) -> String:
101	  match n:
102	    case Node{k, _, _}:
103	      k
104	
105	def ckey(c: Container) -> String:
106	  match c:
107	    case Container{k, _, _, _, _, _, _}:
108	      k
109	
110	def con(c: Container) -> String:
111	  match c:
112	    case Container{_, _, _, _, o, _, _}:
113	      o
114	
115	def caps(c: Container) -> List<&2, Cap>:
116	  match c:
117	    case Container{_, _, _, _, _, _, cs}:
118	      cs
119	
120	def pkey(p: Part) -> String:
121	  match p:
122	    case Part{k, _, _, _}:
123	      k
124	
125	def pin(p: Part) -> String:
126	  match p:
127	    case Part{_, _, _, i}:
128	      i
129	
130	def nkeys(xs: List<&2, Node>) -> List<&2, String>:
131	  match xs:
132	    case []:
133	      []
134	    case n <> rest:
135	      nkey(n) <> nkeys(rest)
136	
137	def ckeys(xs: List<&2, Container>) -> List<&2, String>:
138	  match xs:
139	    case []:
140	      []
141	    case c <> rest:
142	      ckey(c) <> ckeys(rest)
143	
144	def 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.
152	def keys(+s: System) -> List<&2, String>:
153	  List.append(&2, String, ckeys(containers(s)), pkeys(parts(s)))
154	
155	# ---- predicates on the vocabulary ----
156	def is_server(r: NodeRole) -> Bool:
157	  match r:
158	    case Server{}:
159	      True{}
160	    case _:
161	      False{}
162	
163	def is_outside(r: NodeRole) -> Bool:
164	  match r:
165	    case Outside{}:
166	      True{}
167	    case _:
168	      False{}
169	
170	def is_device(r: NodeRole) -> Bool:
171	  match r:
172	    case UserDevice{}:
173	      True{}
174	    case _:
175	      False{}
176	
177	def is_client(k: ContainerKind) -> Bool:
178	  match k:
179	    case Client{}:
180	      True{}
181	    case _:
182	      False{}
183	
184	def is_data_api(k: ContainerKind) -> Bool:
185	  match k:
186	    case DataApi{}:
187	      True{}
188	    case _:
189	      False{}
190	
191	def is_ours(o: Owner) -> Bool:
192	  match o:
193	    case Ours{}:
194	      True{}
195	    case Theirs{}:
196	      False{}
197	
198	def is_local(e: Exposure) -> Bool:
199	  match e:
200	    case Local{}:
201	      True{}
202	    case _:
203	      False{}
204	
205	def is_tailnet(e: Exposure) -> Bool:
206	  match e:
207	    case Tailnet{}:
208	      True{}
209	    case _:
210	      False{}
211	
212	def is_rust(l: Lang) -> Bool:
213	  match l:
214	    case Rust{}:
215	      True{}
216	    case _:
217	      False{}
218	
219	# ---- keys, like foreign keys ----
220	def str_eq(a: String, b: String) -> Bool:
221	  String.eq(a, b)
222	
223	def 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	
230	def 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.
238	def 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`.
246	def 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	
253	def 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	
260	def 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	
267	def 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.
278	def 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 ----
285	def 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.
293	def home(+k: String, +s: System) -> String:
294	  pick_str(has(k, ckeys(containers(s))), k, part_home(k, parts(s)))
295	
296	def none() -> Container:
297	  Container{"", "", Worker{}, Theirs{}, "", Public{}, []}
298	
299	def 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).
307	def 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	
314	def pick_r(hit: Bool, r: NodeRole, other: NodeRole) -> NodeRole:
315	  match hit:
316	    case True{}:
317	      r
318	    case False{}:
319	      other
320	
321	def 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.
331	def node_of(+k: String, +s: System) -> String:
332	  con(container(home(k, s), containers(s)))
333	
334	def 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.
339	def 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	
344	def 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	
351	def 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.
355	def 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	
364	def 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 ----
368	def 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	
383	def one_if(b: Bool) -> Nat:
384	  match b:
385	    case True{}:
386	      1n
387	    case False{}:
388	      0n
389	
390	def 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	
397	def 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.
405	def 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	
412	def 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.
422	def tailnet_data_apis(+s: System) -> Nat:
423	  tailnet_data_apis.go(containers(s))
424	
425	def 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.
435	def 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.
439	def 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	
444	def 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	
451	def 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 ----
455	def backend(c: Container) -> Bool:
456	  match c:
457	    case Container{_, _, kind, owner, _, _, _}:
458	      is_ours(owner) && Bool.not(is_client(kind))
459	
460	def 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	
465	def 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	
472	def 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 ----
476	def 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	
479	def 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	
488	def 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	
495	def container_box(c: Container) -> String:
496	  match c:
497	    case Container{k, name, _, _, on, _, _}:
498	      on ++ "." ++ k ++ ": \"" ++ name ++ "\" {class: container}\n"
499	
500	def 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	
507	def part_box(p: Part, +s: System) -> String:
508	  match p:
509	    case Part{+k, name, _, _}:
510	      path(k, s) ++ ": \"" ++ name ++ "\" {class: part}\n"
511	
512	def 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	
519	def style(live: Bool) -> String:
520	  match live:
521	    case True{}:
522	      "live"
523	    case False{}:
524	      "plain"
525	
526	def 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	
535	def 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)