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

Adds `deploy/hetzner/` — the complete unit for running the public
ECHIDNA API on a single server behind Caddy, plus an operator runbook.

`echidna` (`ghcr.io/hyperpolymath/echidna:latest`, `server --port 8081`)
and `caddy` (built on-box with `mholt/caddy-ratelimit`) run as rootless
podman systemd quadlets on a shared network. Caddy terminates TLS for
`api.nesy-prover.dev` and is the only thing that can reach the API.

## Caging an unauthenticated prover service

The API has no authentication and spawns prover binaries on
user-supplied input with no per-request timeout, so the deployment
constrains it: **no published host port**, 30 req/min/IP rate limit, 1
MB request-body cap, `--memory=1500m --pids-limit=512`, `tmpfs /tmp`,
`NoNewPrivileges`, rootless. (A server-side prover timeout belongs in
the code — worth a follow-up issue.)

## Review fixes already applied

- runbook ran `scp` before the target directories existed — a verbatim
run failed on the first copy
- the auto-update rollback claim was **not true as configured**: an
unhealthy-but-running container satisfies systemd, so nothing failed and
nothing rolled back. `HealthOnFailure=kill` now fails the unit on an
unhealthy container, which is what makes both `Restart=always` and
auto-update's rollback fire
- manual rollback was silently undone by the next
`podman-auto-update.timer` run re-pulling `:latest` — the procedure now
stops the timer first and documents pinned mode as the durable exit
- the `podman >= 4.4` floor was a guess these units do not satisfy. It
is replaced by a **measurement**: preflight runs the quadlet generator
in dry-run mode on the target host, proving every key is understood
regardless of version

## Verification

- `quadlet -dryrun` generates all three units with no warnings; the
resulting `ExecStart` carries `--health-on-failure kill`, tmpfs,
`no-new-privileges`, the autoupdate label, and both limits
- the Caddy image builds with podman, and `caddy validate` accepts the
Caddyfile with `http.handlers.rate_limit` present
- `ghcr.io/hyperpolymath/echidna:latest` confirmed **anonymously
pullable** — no registry credentials needed on the server
- `asciidoctor` renders the runbook with no warnings

Deployment itself is not part of this PR: it needs the server's SSH
details and a Cloudflare token for the `api` A record.

Author: hyperpolymath

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
+		}
+	}
+}

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

deploy/hetzner/README.adoc

@@ -0,0 +1,254 @@
+// 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`.
+* *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)
+
+[source,console]
+----
+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.
+* At least 2 GB RAM. The API container is capped at 1500 MB
+  (`PodmanArgs=--memory=1500m`), deliberately below the host total so
+  Caddy and the OS keep headroom; raise both together if you want more.
+  The `:full` image (Isabelle/Agda/Julia) needs >= 4 GB and is not
+  deployed here.
+* *Quadlet keys are all understood by the installed podman.* Do not
+  trust a version number for this — measure it. Copy the three unit
+  files to the server and run the generator in dry-run mode:
++
+[source,console]
+----
+scp echidna.network echidna.container caddy.container <user>@<SERVER_IP>:/tmp/qcheck/
+ssh <user>@<SERVER_IP> 'QUADLET_UNIT_DIRS=/tmp/qcheck /usr/libexec/podman/quadlet -dryrun'
+----
++
+It must print generated `[Service]` sections for all three units with
+no warnings. These units were authored and dry-run verified against podman
+5.4; podman 5.x is recommended and 4.x is likely to reject at least
+one key (`HealthOnFailure=` in particular). If the dry-run complains,
+use the Debian-12 fallback in the appendix instead.
+* Image pullable anonymously:
++
+[source,console]
+----
+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)
+
+[source,console]
+----
+apt update && apt upgrade -y
+apt install -y podman unattended-upgrades ufw
+dpkg-reconfigure -f noninteractive unattended-upgrades
+
+# Firewall: SSH + HTTP(S) only
+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
+
+# Destination for the Caddyfile and the Caddy build context
+mkdir -p /opt/echidna && chown deploy:deploy /opt/echidna
+----
+
+== 2. Install the deploy unit
+
+Create the quadlet directory *before* copying anything into it — as
+the deploy user on the server:
+
+[source,console]
+----
+mkdir -p ~/.config/containers/systemd
+----
+
+Then, from your workstation in this directory:
+
+[source,console]
+----
+scp Caddyfile Containerfile.caddy deploy@<SERVER_IP>:/opt/echidna/
+scp echidna.network echidna.container caddy.container \
+    deploy@<SERVER_IP>:~/.config/containers/systemd/
+----
+
+Back on the server, as deploy:
+
+[source,console]
+----
+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:
+
+[source]
+----
+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
+
+[source,console]
+----
+systemctl --user start echidna caddy
+podman ps                                   # both Up, echidna (healthy)
+journalctl --user -u caddy -f               # watch certificate issuance
+----
+
+End-to-end, from anywhere:
+
+[source,console]
+----
+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:
+
+[source,console]
+----
+# 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: the API port must NOT be reachable directly. This probe is
+# deliberately plaintext against the raw port — it is asserting that
+# nothing answers there, and must fail.
+curl -m 5 http://<SERVER_IP>:8081/api/health && echo "REACHABLE - FIX THIS" || echo "unreachable (correct)"
+----
+
+Reboot survival (validates linger + `[Install]` + Restart in one shot):
+
+[source,console]
+----
+sudo reboot
+# after it returns:
+podman ps && curl -s https://api.nesy-prover.dev/api/health
+----
+
+== 5. Updates and rollback
+
+`ghcr-publish.yml` pushes a new `:latest` on every GitHub release.
+Enable unattended rollout:
+
+[source,console]
+----
+systemctl --user enable --now podman-auto-update.timer
+podman auto-update --dry-run     # see what would change
+podman auto-update               # roll out immediately
+----
+
+How the safety net actually works: `podman auto-update` pulls the new
+image and restarts the unit. `HealthOnFailure=kill` in
+`echidna.container` means a container that goes unhealthy is killed,
+which fails the systemd unit — and auto-update rolls the unit back to
+the image it was running before when the restarted unit does not come
+up healthy. Without that key an unhealthy-but-running container would
+satisfy systemd and no rollback would occur, so do not remove it.
+
+Manual rollback to a recorded digest. *Stop the timer first* —
+otherwise its next run pulls registry `:latest` again and silently
+undoes the rollback:
+
+[source,console]
+----
+systemctl --user disable --now podman-auto-update.timer
+podman pull ghcr.io/hyperpolymath/echidna@<DIGEST>
+podman tag  ghcr.io/hyperpolymath/echidna@<DIGEST> ghcr.io/hyperpolymath/echidna:latest
+systemctl --user restart echidna
+----
+
+Re-enable the timer only once a fixed `:latest` has been published,
+or switch to pinned mode permanently: set `Image=` in
+`echidna.container` to a `:vX.Y.Z` tag or digest, drop
+`AutoUpdate=registry`, and bump it via PR.
+
+== Appendix: fallback for podman without quadlet support
+
+[source,console]
+----
+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 \
+  --health-on-failure kill \
+  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
+----

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

deploy/hetzner/echidna.container

@@ -0,0 +1,41 @@
+# 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
+# kill (not stop) is what integrates with systemd: an unhealthy
+# container fails the unit, which is what makes Restart=always and
+# podman-auto-update's rollback actually trigger.
+HealthOnFailure=kill
+Tmpfs=/tmp:rw,size=256m
+NoNewPrivileges=true
+PodmanArgs=--memory=1500m --pids-limit=512
+
+[Service]
+Restart=always
+RestartSec=5
+
+[Install]
+WantedBy=default.target

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