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. 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	  AgentApi{}
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_device(r: NodeRole) -> Bool:
164	  match r:
165	    case UserDevice{}:
166	      True{}
167	    case _:
168	      False{}
169	
170	def is_client(k: ContainerKind) -> Bool:
171	  match k:
172	    case Client{}:
173	      True{}
174	    case _:
175	      False{}
176	
177	def is_data_api(k: ContainerKind) -> Bool:
178	  match k:
179	    case DataApi{}:
180	      True{}
181	    case _:
182	      False{}
183	
184	def is_ours(o: Owner) -> Bool:
185	  match o:
186	    case Ours{}:
187	      True{}
188	    case Theirs{}:
189	      False{}
190	
191	def is_local(e: Exposure) -> Bool:
192	  match e:
193	    case Local{}:
194	      True{}
195	    case _:
196	      False{}
197	
198	def is_tailnet(e: Exposure) -> Bool:
199	  match e:
200	    case Tailnet{}:
201	      True{}
202	    case _:
203	      False{}
204	
205	def is_rust(l: Lang) -> Bool:
206	  match l:
207	    case Rust{}:
208	      True{}
209	    case _:
210	      False{}
211	
212	# ---- keys, like foreign keys ----
213	def str_eq(a: String, b: String) -> Bool:
214	  String.eq(a, b)
215	
216	def 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	
223	def 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.
231	def 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`.
239	def 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	
246	def 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	
253	def 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	
260	def 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.
271	def 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 ----
278	def 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.
286	def home(+k: String, +s: System) -> String:
287	  pick_str(has(k, ckeys(containers(s))), k, part_home(k, parts(s)))
288	
289	def none() -> Container:
290	  Container{"", "", Worker{}, Theirs{}, "", Public{}, []}
291	
292	def 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).
300	def 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	
307	def pick_r(hit: Bool, r: NodeRole, other: NodeRole) -> NodeRole:
308	  match hit:
309	    case True{}:
310	      r
311	    case False{}:
312	      other
313	
314	def 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.
324	def node_of(+k: String, +s: System) -> String:
325	  con(container(home(k, s), containers(s)))
326	
327	def 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.
332	def 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	
337	def 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	
344	def 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.
348	def 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	
357	def 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 ----
361	def 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	
376	def one_if(b: Bool) -> Nat:
377	  match b:
378	    case True{}:
379	      1n
380	    case False{}:
381	      0n
382	
383	def 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	
390	def 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.
398	def 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	
405	def 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.
415	def 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.
419	def 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	
424	def 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	
431	def 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 ----
435	def backend(c: Container) -> Bool:
436	  match c:
437	    case Container{_, _, kind, owner, _, _, _}:
438	      is_ours(owner) && Bool.not(is_client(kind))
439	
440	def 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	
445	def 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	
452	def 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 ----
456	def 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	
459	def 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	
468	def 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	
475	def container_box(c: Container) -> String:
476	  match c:
477	    case Container{k, name, _, _, on, _, _}:
478	      on ++ "." ++ k ++ ": \"" ++ name ++ "\" {class: container}\n"
479	
480	def 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	
487	def part_box(p: Part, +s: System) -> String:
488	  match p:
489	    case Part{+k, name, _, _}:
490	      path(k, s) ++ ": \"" ++ name ++ "\" {class: part}\n"
491	
492	def 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	
499	def style(live: Bool) -> String:
500	  match live:
501	    case True{}:
502	      "live"
503	    case False{}:
504	      "plain"
505	
506	def 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	
515	def 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)