domain/architecture/system/deployment/nix_darwin/ops.bend

near-v-framework@0.4.0.0 · 186 lines · 31 definitions

1import Base
2import near-v-framework@0.4.0.0/domain/architecture/system/deployment/nix_darwin/type.bend as ND
3import near-v-framework@0.4.0.0/domain/architecture/system/deployment/nix_darwin/service/type.bend as Sv
4import near-v-framework@0.4.0.0/domain/architecture/system/deployment/nix_darwin/service/ops.bend as SvO
5import near-v-framework@0.4.0.0/domain/architecture/system/container/type.bend as Ct
6
7def user(nd: ND.NixDarwin) -> String:
8  match nd:
9    case ND.NixDarwin{_, _, u, _, _, _, _, _, _, _, _, _, _, _}:
10      u
11
12def tailscale(nd: ND.NixDarwin) -> Bool:
13  match nd:
14    case ND.NixDarwin{_, _, _, _, t, _, _, _, _, _, _, _, _, _}:
15      t
16
17def services(nd: ND.NixDarwin) -> List<&2, Sv.Service>:
18  match nd:
19    case ND.NixDarwin{_, _, _, _, _, _, _, _, ss, _, _, _, _, _}:
20      ss
21
22def serves(nd: ND.NixDarwin) -> List<&2, ND.Serve>:
23  match nd:
24    case ND.NixDarwin{_, _, _, _, _, _, _, _, _, ss, _, _, _, _}:
25      ss
26
27def listeners(nd: ND.NixDarwin) -> List<&2, ND.Listening>:
28  match nd:
29    case ND.NixDarwin{_, _, _, _, _, _, _, _, _, _, ls, _, _, _}:
30      ls
31
32def kept(nd: ND.NixDarwin) -> List<&2, String>:
33  match nd:
34    case ND.NixDarwin{_, _, _, _, _, _, _, _, _, _, _, k, _, _}:
35      k
36
37def serve_container(s: ND.Serve) -> String:
38  match s:
39    case ND.Serve{c, _, _, _}:
40      c
41
42def serve_https(s: ND.Serve) -> U32:
43  match s:
44    case ND.Serve{_, h, _, _}:
45      h
46
47def serve_port(s: ND.Serve) -> U32:
48  match s:
49    case ND.Serve{_, _, p, _}:
50      p
51
52# What Tailscale proxies a serve to.
53def 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
58def listening_process(l: ND.Listening) -> String:
59  match l:
60    case ND.Listening{p, _}:
61      p
62
63def 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 ----
71def 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.
79def 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.
94def 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.
99def 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
102def distinct(ps: List<&2, U32>) -> Bool:
103  match ps:
104    case []:
105      True{}
106    case +p <> +rest:
107      fresh(p, rest) && distinct(rest)
108
109def 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.
117def serve_ports_distinct(nd: ND.NixDarwin) -> Bool:
118  distinct(https_ports(serves(nd)))
119
120def 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
125def 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).
133def listeners_belong(nd: ND.NixDarwin, +keys: List<&2, String>) -> Bool:
134  all_belong(listeners(nd), keys)
135
136def 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
143def 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.
151def services_on(+nd: ND.NixDarwin, +instances: List<&2, String>) -> Bool:
152  services_among(services(nd), instances) && serves_among(serves(nd), instances)
153
154def 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
161def is_tailnet(e: Ct.Exposure) -> Bool:
162  match e:
163    case Ct.Tailnet{}:
164      True{}
165    case _:
166      False{}
167
168def 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
173def 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.
181def 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.
185def 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))