feat(deploy): Hetzner deploy unit for api.nesy-prover.dev

hyperpolymath · claude · hyperpolymath · commit b2b2a148256b · 2026-07-28T15:42:50.000+01:00
Complete single-box deployment for the public API: rootless podman
systemd quadlets (echidna API + Caddy TLS proxy), a Caddy image built
on-host with mholt/caddy-ratelimit, and an operator runbook.

The API is unauthenticated and spawns prover binaries on user input,
so it is caged: no published host port (Caddy-only reachability over
the quadlet network), 30 req/min/IP rate limit, 1 MB body cap,
memory/pids limits, tmpfs /tmp, NoNewPrivileges. Updates roll out via
podman-auto-update with healthcheck-gated rollback.

Verified locally: quadlet -dryrun generates all three units with zero
warnings and correct dependency ordering; the Caddy image builds with
podman and 'caddy validate' accepts the Caddyfile with
http.handlers.rate_limit present.

Co-Authored-By: Claude Fable 5 &lt;noreply@anthropic.com&gt;
diff --git a/deploy/hetzner/Caddyfile b/deploy/hetzner/Caddyfile
@@ -0,0 +1,44 @@
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# TLS-terminating reverse proxy for the public ECHIDNA API.
+# Runs in the localhost/caddy-rl:2 image (see Containerfile.caddy);
+# the rate_limit directive is provided by mholt/caddy-ratelimit.
+
+{
+	email j.d.a.jewell@open.ac.uk
+	order rate_limit before reverse_proxy
+}
+
+api.nesy-prover.dev {
+	encode zstd gzip
+
+	# The API executes prover input; cap request size and per-client
+	# rate before anything reaches it.
+	request_body {
+		max_size 1MB
+	}
+	rate_limit {
+		zone api {
+			key {remote_host}
+			events 30
+			window 1m
+		}
+	}
+
+	header {
+		Strict-Transport-Security "max-age=31536000"
+		X-Content-Type-Options nosniff
+		X-Frame-Options DENY
+		Referrer-Policy no-referrer
+		-Server
+	}
+
+	# `echidna` resolves on the shared podman network (echidna.network);
+	# the API container publishes no host port.
+	reverse_proxy echidna:8081 {
+		transport http {
+			response_header_timeout 120s
+		}
+	}
+}
diff --git a/deploy/hetzner/Containerfile.caddy b/deploy/hetzner/Containerfile.caddy
@@ -0,0 +1,15 @@
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# Caddy with the mholt/caddy-ratelimit plugin (stock Caddy has no rate
+# limiting). Built on the target host with podman — never published:
+#
+#     podman build -f Containerfile.caddy -t localhost/caddy-rl:2 .
+#
+# RSR-H15: podman + Containerfile, not Docker.
+
+FROM docker.io/library/caddy:2-builder AS builder
+RUN xcaddy build --with github.com/mholt/caddy-ratelimit
+
+FROM docker.io/library/caddy:2
+COPY --from=builder /usr/bin/caddy /usr/bin/caddy
diff --git a/deploy/hetzner/README.adoc b/deploy/hetzner/README.adoc
@@ -0,0 +1,181 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= Deploying the ECHIDNA API to Hetzner (api.nesy-prover.dev)
+:toc:
+:toclevels: 2
+
+This directory is the complete deploy unit for running the public
+ECHIDNA API on a single Hetzner server behind Caddy (auto-TLS via
+Let's Encrypt), orchestrated with podman systemd quadlets.
+
+.What runs where
+[cols="1,3"]
+|===
+| `echidna`  | `ghcr.io/hyperpolymath/echidna:latest`, `server --port 8081 --host 0.0.0.0 --cors`. No published host port — reachable only from Caddy over the `echidna-net` podman network.
+| `caddy`    | `localhost/caddy-rl:2` (built on-box from `Containerfile.caddy`), ports 80/443, terminates TLS for `api.nesy-prover.dev`, rate-limits (30 req/min/IP), caps request bodies at 1 MB.
+|===
+
+== Decision record
+
+* *Quadlets over podman-compose*: systemd-native restart-on-boot with no
+  extra daemon, unit-level dependency ordering, and first-class
+  `AutoUpdate=registry` integration with `podman-auto-update.timer`
+  (which rolls back automatically when the updated container fails its
+  healthcheck). Requires podman >= 4.4.
+* *Rootless*: the API executes user-supplied prover input; run both
+  units as an unprivileged `deploy` user with linger.
+* *Caddy over svalinn*: the estate's svalinn/vordr stack is not yet
+  CI-proven; Caddy is the low-risk choice for a public endpoint. The
+  `container/compose.toml` selur stack remains for local development.
+* *No API auth at launch*: the service is deliberately public but caged
+  (rate limit, body cap, memory/pids limits, tmpfs, unpublished port).
+  If abuse appears, add a bearer-token matcher in the Caddyfile for
+  POST routes. A server-side per-request prover timeout is tracked as a
+  follow-up issue in the main repo.
+
+== 0. Preflight (read-only, do first)
+
+  ssh <user>@<SERVER_IP> 'cat /etc/os-release; free -h; df -h /; nproc; ss -tlnp; podman --version'
+
+Gates — stop and reassess if any fail:
+
+* Ports 80/443 unbound (`ss -tlnp` shows no listener). If something
+  else owns them, this plan does not apply as-is.
+* >= 2 GB RAM free for the `:latest` image (Z3 + Lean). The `:full`
+  image (Isabelle/Agda/Julia) needs >= 4 GB and is not deployed here.
+* podman >= 4.4 for quadlets. Debian 12 ships 4.3.1 — either install a
+  newer podman or fall back to `podman generate systemd --new --files`
+  (same containers, generated units instead of quadlets).
+* Image pullable anonymously:
++
+  podman manifest inspect ghcr.io/hyperpolymath/echidna:latest
++
+On 401: make the GHCR package public (GitHub → Packages → echidna →
+Package settings → visibility) or use a read-only PAT with
+`podman login ghcr.io` as the deploy user.
+
+== 1. Server preparation (as root)
+
+  apt update && apt upgrade -y
+  apt install -y podman unattended-upgrades
+  dpkg-reconfigure -f noninteractive unattended-upgrades
+
+  # Firewall: SSH + HTTP(S) only
+  apt install -y ufw
+  ufw default deny incoming
+  ufw allow 22/tcp && ufw allow 80/tcp && ufw allow 443/tcp
+  ufw enable
+
+  # Unprivileged deploy user with lingering services
+  useradd -m -s /bin/bash deploy
+  loginctl enable-linger deploy
+
+  # Let rootless podman bind 80/443
+  echo 'net.ipv4.ip_unprivileged_port_start=80' > /etc/sysctl.d/50-unprivileged-ports.conf
+  sysctl --system
+
+== 2. Install the deploy unit (as deploy)
+
+From your workstation, from this directory:
+
+  scp Caddyfile Containerfile.caddy deploy@<SERVER_IP>:/opt/echidna/
+  scp echidna.network echidna.container caddy.container \
+      deploy@<SERVER_IP>:~/.config/containers/systemd/
+
+(Create the target dirs first: `sudo mkdir -p /opt/echidna && sudo chown deploy /opt/echidna`
+and `mkdir -p ~/.config/containers/systemd` as deploy.)
+
+On the server, as deploy:
+
+  cd /opt/echidna
+  podman build -f Containerfile.caddy -t localhost/caddy-rl:2 .
+  podman pull ghcr.io/hyperpolymath/echidna:latest
+  podman image inspect --format '{{.Digest}}' ghcr.io/hyperpolymath/echidna:latest
+  # ^ record this digest in env.example / your notes for rollback
+
+  systemctl --user daemon-reload
+  systemctl --user list-unit-files | grep -E 'echidna|caddy'
+
+== 3. DNS (before starting Caddy)
+
+Create in the Cloudflare zone for nesy-prover.dev:
+
+  A  api  <SERVER_IP>  proxied=false (grey cloud), TTL 300
+
+Grey cloud is required at launch so Caddy's Let's Encrypt HTTP-01
+challenge reaches the server directly. (Optional later hardening:
+orange-cloud + a Cloudflare Origin CA cert in the Caddyfile.)
+
+Wait until `dig +short api.nesy-prover.dev @1.1.1.1` returns the
+server IP before the first Caddy start — ACME then succeeds first try.
+
+== 4. Bring-up and verification
+
+  systemctl --user start echidna caddy
+  podman ps                                   # both Up, echidna (healthy)
+  journalctl --user -u caddy -f               # watch certificate issuance
+
+End-to-end, from anywhere:
+
+  curl -s https://api.nesy-prover.dev/api/health        # {"status":"ok",...}
+  curl -s https://api.nesy-prover.dev/api/provers | head
+  curl -s -X POST https://api.nesy-prover.dev/api/verify \
+    -H 'content-type: application/json' \
+    -d '{"prover":"Z3","content":"(assert (forall ((x Int)) (= (+ x 0) x)))(check-sat)"}'
+
+Controls:
+
+  # Rate limit: burst 40 requests, expect HTTP 429 after ~30
+  for i in $(seq 1 40); do curl -s -o /dev/null -w '%{http_code} ' \
+    https://api.nesy-prover.dev/api/health; done; echo
+  # Headers: HSTS present, Server header absent
+  curl -sI https://api.nesy-prover.dev/api/health
+  # Isolation: direct API port must be unreachable from outside
+  curl -m 5 http://<SERVER_IP>:8081/api/health || echo "unreachable (correct)"
+
+Reboot survival (validates linger + [Install] + Restart in one shot):
+
+  sudo reboot
+  # after it returns:
+  podman ps && curl -s https://api.nesy-prover.dev/api/health
+
+== 5. Updates and rollback
+
+Enable unattended rollout of new releases (ghcr-publish.yml pushes
+`:latest` on every GitHub release):
+
+  systemctl --user enable --now podman-auto-update.timer
+  podman auto-update --dry-run     # see what would change
+  podman auto-update               # roll out immediately
+
+`podman-auto-update` restarts the unit on a new image and rolls back
+automatically if the fresh container fails its healthcheck.
+
+Manual rollback to a recorded digest:
+
+  podman pull ghcr.io/hyperpolymath/echidna@<DIGEST>
+  podman tag  ghcr.io/hyperpolymath/echidna@<DIGEST> ghcr.io/hyperpolymath/echidna:latest
+  systemctl --user restart echidna
+
+Pinned mode (opt out of auto-update): set `Image=` in
+`echidna.container` to a `:vX.Y.Z` tag or digest, remove
+`AutoUpdate=registry`, and bump via PR.
+
+== Appendix: Debian 12 fallback (podman 4.3, no quadlets)
+
+  podman network create echidna-net
+  podman create --name echidna --network echidna-net \
+    --memory=1500m --pids-limit=512 --tmpfs /tmp:rw,size=256m \
+    --security-opt no-new-privileges \
+    --health-cmd '/app/bin/echidna --version' --health-interval 30s \
+    ghcr.io/hyperpolymath/echidna:latest server --port 8081 --host 0.0.0.0 --cors
+  podman create --name caddy --network echidna-net \
+    -p 80:80 -p 443:443 \
+    -v /opt/echidna/Caddyfile:/etc/caddy/Caddyfile:ro \
+    -v caddy-data:/data -v caddy-config:/config \
+    localhost/caddy-rl:2
+  podman generate systemd --new --files --name echidna
+  podman generate systemd --new --files --name caddy
+  mkdir -p ~/.config/systemd/user && mv container-*.service ~/.config/systemd/user/
+  systemctl --user daemon-reload
+  systemctl --user enable --now container-echidna container-caddy
diff --git a/deploy/hetzner/caddy.container b/deploy/hetzner/caddy.container
@@ -0,0 +1,31 @@
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# Quadlet unit for the Caddy TLS proxy fronting api.nesy-prover.dev.
+#
+# Build the image on the host first:
+#     podman build -f Containerfile.caddy -t localhost/caddy-rl:2 .
+# The caddy-data volume persists the ACME account and certificates —
+# do not delete it casually (Let's Encrypt rate limits).
+
+[Unit]
+Description=Caddy TLS proxy for api.nesy-prover.dev
+Wants=echidna.service
+After=echidna.service
+
+[Container]
+Image=localhost/caddy-rl:2
+ContainerName=caddy
+Network=echidna.network
+PublishPort=80:80
+PublishPort=443:443
+Volume=/opt/echidna/Caddyfile:/etc/caddy/Caddyfile:ro
+Volume=caddy-data:/data
+Volume=caddy-config:/config
+
+[Service]
+Restart=always
+RestartSec=5
+
+[Install]
+WantedBy=default.target
diff --git a/deploy/hetzner/echidna.container b/deploy/hetzner/echidna.container
@@ -0,0 +1,37 @@
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# Quadlet unit for the ECHIDNA API server.
+#
+# The API has no authentication and spawns prover binaries on user
+# input, so it is caged: no published host port (only Caddy reaches it
+# over echidna-net), memory/pids limits, tmpfs /tmp, no privilege
+# escalation. Healthcheck uses the binary — the image ships no curl.
+#
+# Image tag :latest is intentional together with AutoUpdate=registry +
+# podman-auto-update.timer: new releases roll out automatically and a
+# failing healthcheck rolls back. For pinned mode, set Image= to a
+# :vX.Y.Z tag or digest and bump via PR (see README.adoc).
+
+[Unit]
+Description=ECHIDNA theorem-prover API
+
+[Container]
+Image=ghcr.io/hyperpolymath/echidna:latest
+AutoUpdate=registry
+ContainerName=echidna
+Network=echidna.network
+Exec=server --port 8081 --host 0.0.0.0 --cors
+Environment=RUST_LOG=info
+HealthCmd=/app/bin/echidna --version
+HealthInterval=30s
+Tmpfs=/tmp:rw,size=256m
+NoNewPrivileges=true
+PodmanArgs=--memory=1500m --pids-limit=512
+
+[Service]
+Restart=always
+RestartSec=5
+
+[Install]
+WantedBy=default.target
diff --git a/deploy/hetzner/echidna.network b/deploy/hetzner/echidna.network
@@ -0,0 +1,9 @@
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# Shared podman network for the API + proxy pair. Referenced by name
+# (echidna.network) from both .container units so systemd orders
+# creation correctly.
+
+[Network]
+NetworkName=echidna-net
diff --git a/deploy/hetzner/env.example b/deploy/hetzner/env.example
@@ -0,0 +1,18 @@
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# Values that vary per deployment. Nothing here is secret by design —
+# the API takes no credentials; Cloudflare tokens are used from the
+# operator's workstation, never stored on the server.
+
+# Public IPv4 of the Hetzner server (target of the api A record).
+SERVER_IP=
+
+# Image reference actually deployed. :latest is the auto-update mode;
+# record the digest at deploy time for rollback:
+#     podman image inspect --format '{{.Digest}}' ghcr.io/hyperpolymath/echidna:latest
+ECHIDNA_IMAGE=ghcr.io/hyperpolymath/echidna:latest
+ECHIDNA_IMAGE_DIGEST=
+
+# ACME/Let's Encrypt contact (also set in the Caddyfile global block).
+ACME_EMAIL=j.d.a.jewell@open.ac.uk
