1	import Base
2	import ./type.bend as ND
3	import ./service/type.bend as Sv
4	import ./service/ops.bend as SvO
5	import ../../container/type.bend as Ct
6	
7	def user(nd: ND.NixDarwin) -> String:
8	  match nd:
9	    case ND.NixDarwin{_, _, u, _, _, _, _, _, _, _, _, _, _, _}:
10	      u
11	
12	def tailscale(nd: ND.NixDarwin) -> Bool:
13	  match nd:
14	    case ND.NixDarwin{_, _, _, _, t, _, _, _, _, _, _, _, _, _}:
15	      t
16	
17	def services(nd: ND.NixDarwin) -> List<&2, Sv.Service>:
18	  match nd:
19	    case ND.NixDarwin{_, _, _, _, _, _, _, _, ss, _, _, _, _, _}:
20	      ss
21	
22	def serves(nd: ND.NixDarwin) -> List<&2, ND.Serve>:
23	  match nd:
24	    case ND.NixDarwin{_, _, _, _, _, _, _, _, _, ss, _, _, _, _}:
25	      ss
26	
27	def listeners(nd: ND.NixDarwin) -> List<&2, ND.Listening>:
28	  match nd:
29	    case ND.NixDarwin{_, _, _, _, _, _, _, _, _, _, ls, _, _, _}:
30	      ls
31	
32	def kept(nd: ND.NixDarwin) -> List<&2, String>:
33	  match nd:
34	    case ND.NixDarwin{_, _, _, _, _, _, _, _, _, _, _, k, _, _}:
35	      k
36	
37	def serve_container(s: ND.Serve) -> String:
38	  match s:
39	    case ND.Serve{c, _, _, _}:
40	      c
41	
42	def serve_https(s: ND.Serve) -> U32:
43	  match s:
44	    case ND.Serve{_, h, _, _}:
45	      h
46	
47	def serve_port(s: ND.Serve) -> U32:
48	  match s:
49	    case ND.Serve{_, _, p, _}:
50	      p
51	
52	# What Tailscale proxies a serve to.
53	def serve_target(s: ND.Serve) -> String:
54	  match s:
55	    case ND.Serve{_, _, p, path}:
56	      "http://127.0.0.1:" ++ U32.show(p) ++ path
57	
58	def listening_process(l: ND.Listening) -> String:
59	  match l:
60	    case ND.Listening{p, _}:
61	      p
62	
63	def listening_processes(xs: List<&2, ND.Listening>) -> List<&2, String>:
64	  match xs:
65	    case []:
66	      []
67	    case l <> rest:
68	      listening_process(l) <> listening_processes(rest)
69	
70	# ---- the nix-darwin flake: pinned inputs, the Mac's module, and one launchd job per service ----
71	def tailscale_line(on: Bool) -> String:
72	  match on:
73	    case True{}:
74	      "      services.tailscale.enable = true;\n"
75	    case False{}:
76	      ""
77	
78	# `lets` are Nix bindings the jobs may use (e.g. a derivation); `config` is extra nix-darwin config lines.
79	def flake(nd: ND.NixDarwin) -> String:
80	  match nd:
81	    case ND.NixDarwin{host, platform, +u, +logs, t, _, _, _, ss, _, _, _, lets, config}:
82	      "# Generated by V from the architecture. Do not edit.\n" ++
83	      "{\n" ++
84	      "  inputs.nixpkgs.url = \"github:NixOS/nixpkgs/nixpkgs-unstable\";\n" ++
85	      "  inputs.nix-darwin.url = \"github:nix-darwin/nix-darwin/master\";\n" ++
86	      "  inputs.nix-darwin.inputs.nixpkgs.follows = \"nixpkgs\";\n" ++
87	      "  outputs = { nixpkgs, nix-darwin, ... }: {\n" ++
88	      "    darwinConfigurations." ++ host ++ " = nix-darwin.lib.darwinSystem {\n" ++
89	      "      system = \"" ++ platform ++ "\";\n" ++
90	      "      modules = [ ./mac.nix ({ pkgs, ... }: let\n" ++ lets ++
91	      "      in {\n" ++ config ++ tailscale_line(t) ++ SvO.jobs(ss, u, logs) ++ "      }) ];\n    };\n  };\n}"
92	
93	# The Tailscale CLI: Nix's when Nix runs Tailscale, else the app's.
94	def tailscale_command(nd: ND.NixDarwin) -> String:
95	  Bool.pick(String, tailscale(nd), "/run/current-system/sw/bin/tailscale", "/Applications/Tailscale.app/Contents/MacOS/Tailscale")
96	
97	# ---- laws of a system with this node ----
98	# 0 is not a port.
99	def fresh(+p: U32, ps: List<&2, U32>) -> Bool:
100	  U32.is_eq(p, 0) || Bool.not(List.contains(~U32, ~U32.is_eq, ps, p))
101	
102	def distinct(ps: List<&2, U32>) -> Bool:
103	  match ps:
104	    case []:
105	      True{}
106	    case +p <> +rest:
107	      fresh(p, rest) && distinct(rest)
108	
109	def https_ports(xs: List<&2, ND.Serve>) -> List<&2, U32>:
110	  match xs:
111	    case []:
112	      []
113	    case s <> rest:
114	      serve_https(s) <> https_ports(rest)
115	
116	# No two serves share a tailnet HTTPS port.
117	def serve_ports_distinct(nd: ND.NixDarwin) -> Bool:
118	  distinct(https_ports(serves(nd)))
119	
120	def belongs(l: ND.Listening, +keys: List<&2, String>) -> Bool:
121	  match l:
122	    case ND.Listening{_, +o}:
123	      String.eq(o, "macos") || List.contains(~String, ~String.eq, keys, o)
124	
125	def all_belong(xs: List<&2, ND.Listening>, +keys: List<&2, String>) -> Bool:
126	  match xs:
127	    case []:
128	      True{}
129	    case l <> rest:
130	      belongs(l, keys) && all_belong(rest, keys)
131	
132	# Every allowed listener belongs to macOS or to one of `keys` (the system's containers and nodes).
133	def listeners_belong(nd: ND.NixDarwin, +keys: List<&2, String>) -> Bool:
134	  all_belong(listeners(nd), keys)
135	
136	def services_among(xs: List<&2, Sv.Service>, +instances: List<&2, String>) -> Bool:
137	  match xs:
138	    case []:
139	      True{}
140	    case s <> rest:
141	      List.contains(~String, ~String.eq, instances, SvO.container(s)) && services_among(rest, instances)
142	
143	def serves_among(xs: List<&2, ND.Serve>, +instances: List<&2, String>) -> Bool:
144	  match xs:
145	    case []:
146	      True{}
147	    case s <> rest:
148	      List.contains(~String, ~String.eq, instances, serve_container(s)) && serves_among(rest, instances)
149	
150	# Services and serves run only containers this node runs.
151	def services_on(+nd: ND.NixDarwin, +instances: List<&2, String>) -> Bool:
152	  services_among(services(nd), instances) && serves_among(serves(nd), instances)
153	
154	def served(+k: String, xs: List<&2, ND.Serve>) -> Bool:
155	  match xs:
156	    case []:
157	      False{}
158	    case s <> rest:
159	      String.eq(k, serve_container(s)) || served(k, rest)
160	
161	def is_tailnet(e: Ct.Exposure) -> Bool:
162	  match e:
163	    case Ct.Tailnet{}:
164	      True{}
165	    case _:
166	      False{}
167	
168	def honest(c: Ct.Container, +ss: List<&2, ND.Serve>, +instances: List<&2, String>) -> Bool:
169	  match c:
170	    case Ct.Container{+k, _, _, _, _, e, _, _, _, _, _, _, _, _, _}:
171	      Bool.not(List.contains(~String, ~String.eq, instances, k)) || Bool.not(Bool.xor(is_tailnet(e), served(k, ss)))
172	
173	def all_honest(cs: List<&2, Ct.Container>, +ss: List<&2, ND.Serve>, +instances: List<&2, String>) -> Bool:
174	  match cs:
175	    case []:
176	      True{}
177	    case c <> rest:
178	      honest(c, ss, instances) && all_honest(rest, ss, instances)
179	
180	# A container on this node is on the tailnet exactly when a serve names it.
181	def exposure_honest(nd: ND.NixDarwin, +cs: List<&2, Ct.Container>, +instances: List<&2, String>) -> Bool:
182	  all_honest(cs, serves(nd), instances)
183	
184	# Services that start at login need the Mac to log its user in by itself.
185	def survives_reboot(+nd: ND.NixDarwin, auto_login_user: String) -> Bool:
186	  Bool.not(SvO.needs_login(services(nd))) || String.eq(auto_login_user, user(nd))