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. 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.
26	type 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.
35	type 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.
40	type 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).
49	type Cap is Data:
50	  Hosting{}
51	  PrivateAccess{}
52	  PrivateHosting{}
53	  Realtime{}
54	  BlobStore{}
55	
56	type Lang is Data:
57	  Rust{}
58	  TypeScript{}
59	  JavaScript{}
60	  Python{}
61	  Opaque{}
62	
63	type Container is Data:
64	  Container{key: String, name: String, kind: ContainerKind, owner: Owner, on: String, exposure: Exposure, caps: List<&2, Cap>}
65	
66	type 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.
70	type Link is Data:
71	  Link{src: String, dst: String, label: String, live: Bool}
72	
73	type System is Data:
74	  System{nodes: List<&2, Node>, containers: List<&2, Container>, parts: List<&2, Part>, links: List<&2, Link>}
75	
76	# ---- access ----
77	def nodes(s: System) -> List<&2, Node>:
78	  match s:
79	    case System{n, _, _, _}:
80	      n
81	
82	def containers(s: System) -> List<&2, Container>:
83	  match s:
84	    case System{_, c, _, _}:
85	      c
86	
87	def parts(s: System) -> List<&2, Part>:
88	  match s:
89	    case System{_, _, p, _}:
90	      p
91	
92	def links(s: System) -> List<&2, Link>:
93	  match s:
94	    case System{_, _, _, l}:
95	      l
96	
97	def nkey(n: Node) -> String:
98	  match n:
99	    case Node{k, _, _}:
100	      k
101	
102	def ckey(c: Container) -> String:
103	  match c:
104	    case Container{k, _, _, _, _, _, _}:
105	      k
106	
107	def con(c: Container) -> String:
108	  match c:
109	    case Container{_, _, _, _, o, _, _}:
110	      o
111	
112	def caps(c: Container) -> List<&2, Cap>:
113	  match c:
114	    case Container{_, _, _, _, _, _, cs}:
115	      cs
116	
117	def pkey(p: Part) -> String:
118	  match p:
119	    case Part{k, _, _, _}:
120	      k
121	
122	def pin(p: Part) -> String:
123	  match p:
124	    case Part{_, _, _, i}:
125	      i
126	
127	def nkeys(xs: List<&2, Node>) -> List<&2, String>:
128	  match xs:
129	    case []:
130	      []
131	    case n <> rest:
132	      nkey(n) <> nkeys(rest)
133	
134	def ckeys(xs: List<&2, Container>) -> List<&2, String>:
135	  match xs:
136	    case []:
137	      []
138	    case c <> rest:
139	      ckey(c) <> ckeys(rest)
140	
141	def 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.
149	def keys(+s: System) -> List<&2, String>:
150	  List.append(&2, String, ckeys(containers(s)), pkeys(parts(s)))
151	
152	# ---- predicates on the vocabulary ----
153	def is_server(r: NodeRole) -> Bool:
154	  match r:
155	    case Server{}:
156	      True{}
157	    case _:
158	      False{}
159	
160	def is_device(r: NodeRole) -> Bool:
161	  match r:
162	    case UserDevice{}:
163	      True{}
164	    case _:
165	      False{}
166	
167	def is_client(k: ContainerKind) -> Bool:
168	  match k:
169	    case Client{}:
170	      True{}
171	    case _:
172	      False{}
173	
174	def is_data_api(k: ContainerKind) -> Bool:
175	  match k:
176	    case DataApi{}:
177	      True{}
178	    case _:
179	      False{}
180	
181	def is_ours(o: Owner) -> Bool:
182	  match o:
183	    case Ours{}:
184	      True{}
185	    case Theirs{}:
186	      False{}
187	
188	def is_local(e: Exposure) -> Bool:
189	  match e:
190	    case Local{}:
191	      True{}
192	    case _:
193	      False{}
194	
195	def is_tailnet(e: Exposure) -> Bool:
196	  match e:
197	    case Tailnet{}:
198	      True{}
199	    case _:
200	      False{}
201	
202	def is_rust(l: Lang) -> Bool:
203	  match l:
204	    case Rust{}:
205	      True{}
206	    case _:
207	      False{}
208	
209	# ---- keys, like foreign keys ----
210	def str_eq(a: String, b: String) -> Bool:
211	  String.eq(a, b)
212	
213	def 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	
220	def 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.
228	def 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`.
236	def 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	
243	def 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	
250	def 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	
257	def 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.
268	def 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 ----
275	def 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.
283	def home(+k: String, +s: System) -> String:
284	  pick_str(has(k, ckeys(containers(s))), k, part_home(k, parts(s)))
285	
286	def none() -> Container:
287	  Container{"", "", Worker{}, Theirs{}, "", Public{}, []}
288	
289	def 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).
297	def 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	
304	def pick_r(hit: Bool, r: NodeRole, other: NodeRole) -> NodeRole:
305	  match hit:
306	    case True{}:
307	      r
308	    case False{}:
309	      other
310	
311	def 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.
321	def node_of(+k: String, +s: System) -> String:
322	  con(container(home(k, s), containers(s)))
323	
324	def 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.
329	def 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	
334	def 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	
341	def 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.
345	def 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	
354	def 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 ----
358	def 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	
373	def one_if(b: Bool) -> Nat:
374	  match b:
375	    case True{}:
376	      1n
377	    case False{}:
378	      0n
379	
380	def 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	
387	def 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.
395	def 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	
402	def 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.
412	def 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.
416	def 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	
421	def 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	
428	def 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 ----
432	def backend(c: Container) -> Bool:
433	  match c:
434	    case Container{_, _, kind, owner, _, _, _}:
435	      is_ours(owner) && Bool.not(is_client(kind))
436	
437	def 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	
442	def 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	
449	def 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 ----
453	def 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	
456	def 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	
465	def 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	
472	def container_box(c: Container) -> String:
473	  match c:
474	    case Container{k, name, _, _, on, _, _}:
475	      on ++ "." ++ k ++ ": \"" ++ name ++ "\" {class: container}\n"
476	
477	def 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	
484	def part_box(p: Part, +s: System) -> String:
485	  match p:
486	    case Part{+k, name, _, _}:
487	      path(k, s) ++ ": \"" ++ name ++ "\" {class: part}\n"
488	
489	def 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	
496	def style(live: Bool) -> String:
497	  match live:
498	    case True{}:
499	      "live"
500	    case False{}:
501	      "plain"
502	
503	def 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	
512	def 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)