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