feat(deploy): public Fly.io instance + ghcr one-liner (Task 6) (#261)

## Summary

- **fly.toml**: convert from internal-only TCP to public
`[http_service]` (HTTPS 443 → :8090); switch build from Dockerfile to
pre-built `ghcr.io/hyperpolymath/echidna:full` image
- **fly-deploy.yml**: new CI workflow — deploys to
`echidna-nesy.fly.dev` on each release and `workflow_dispatch`

## The two delivery forms (both)

### 1. podman one-liner for colleagues (already works — image is live at
v2.3.0)

```bash
# minimal image (Z3 + Lean) — fastest
podman run --rm -p 8081:8081 ghcr.io/hyperpolymath/echidna:latest server --port 8081 --cors

# full image (all provers + Julia ML) — for serious colleagues
podman run --rm -p 8081:8081 ghcr.io/hyperpolymath/echidna:full server --port 8081 --cors
```

Then in another terminal:
```bash
curl -X POST http://localhost:8081/api/prove \
  -H 'content-type: application/json' \
  -d '{"prover":"Z3","content":"(set-logic QF_LIA)\n(declare-const x Int)\n(assert (and (> x 0) (< x 0)))\n(check-sat)\n","timeout":30}'
# → {"success":true,...}
```

### 2. Fly.io public instance — one-time setup needed

```bash
# One-time (you do this once):
flyctl apps create echidna-nesy
flyctl tokens create deploy -a echidna-nesy  # copy the token
gh secret set FLY_API_TOKEN -b"<token>" -R hyperpolymath/echidna

# Then trigger the workflow (or create a release):
gh workflow run fly-deploy.yml --repo hyperpolymath/echidna
```

After deploy: `https://echidna-nesy.fly.dev/api/health`

## Notes

- The internal `.flycast` URL (`echidna-nesy.flycast:8090`) still works
for `proven-nesy-solver-api` — flycast is automatic and unaffected by
adding `[http_service]`
- `flyctl` is not installed on the dev WSL machine; hence the CI
workflow approach
- `FLY_API_TOKEN` must be set as a repo secret before the workflow can
run

## Test plan

- [ ] Add `FLY_API_TOKEN` repo secret
- [ ] Trigger `fly-deploy.yml` via `workflow_dispatch`
- [ ] Confirm `https://echidna-nesy.fly.dev/api/health` returns
`{"status":"ok",...}`
- [ ] Confirm refutation demo returns `success:true`

Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/fly-deploy.yml

@@ -0,0 +1,31 @@
+# SPDX-License-Identifier: MPL-2.0
+# Deploy to Fly.io — runs after each release (once ghcr-publish.yml has pushed
+# ghcr.io/hyperpolymath/echidna:full) and on workflow_dispatch.
+#
+# Prerequisites:
+#   1. App created: flyctl apps create echidna-nesy
+#   2. FLY_API_TOKEN secret set in repo:
+#        flyctl tokens create deploy -a echidna-nesy
+#        gh secret set FLY_API_TOKEN -b"<token>" -R hyperpolymath/echidna
+name: Deploy to Fly.io
+on:
+  release:
+    types: [published]
+  workflow_dispatch:
+permissions:
+  contents: read
+jobs:
+  deploy:
+    name: Deploy echidna-nesy
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v4
+      - name: Install flyctl
+        uses: superfly/flyctl-actions/setup-flyctl@ed8efb33836e8b2096c7fd3ba1c8afe303ebbff1 # main 2025-06
+      - name: Deploy
+        run: flyctl deploy --remote-only -a echidna-nesy
+        env:
+          FLY_API_TOKEN: ${{ secrets.FLY_API_TOKEN }}

fly.toml

@@ -1,53 +1,52 @@
 # SPDX-License-Identifier: MPL-2.0
-# fly.io deployment for echidna (Phase E3 nesy-solver playground backend).
+# fly.io deployment for echidna.
 #
-# Deploy:
-#   flyctl launch --no-deploy --copy-config --name echidna-nesy
-#   flyctl deploy -c fly.toml -f .containerization/Containerfile.full
+# Public HTTPS:  https://echidna-nesy.fly.dev/api/health
+# Internal:      echidna-nesy.flycast:8090  (proven-nesy-solver-api + other Fly apps)
 #
-# Internal-only: echidna is reached via echidna-nesy.flycast:8090 from
-# proven-nesy-solver-api; no public http_service.
-# Use .flycast (not .internal) so Fly auto-wakes the machine on first connection.
+# First deploy (one-time):
+#   flyctl apps create echidna-nesy
+#   flyctl secrets set FLY_API_TOKEN=... -a echidna-nesy  # (CI sets this)
+#   flyctl deploy -a echidna-nesy
 #
-# NB: Container is LARGE (~6-8 GB) — Julia + Idris2 + Agda + Lean + Isabelle.
-# Memory must be >=4GB (Isabelle Main heap ~1GB); shared-cpu-2x is the
-# cheapest size that fits.
+# Subsequent deploys are handled by .github/workflows/fly-deploy.yml on release.
+#
+# NB: Uses the pre-built ghcr.io/hyperpolymath/echidna:full image (published by
+# ghcr-publish.yml on each release) to avoid building the 6-8 GB layer here.
+# Memory >=4 GB required: Isabelle Main heap ~1 GB; Julia JIT overhead.
 
 app = "echidna-nesy"
 primary_region = "lhr"
 kill_signal = "SIGTERM"
 kill_timeout = "10s"
 
 [build]
-  dockerfile = ".containerization/Containerfile.full"
+  image = "ghcr.io/hyperpolymath/echidna:full"
 
 [env]
-  # echidna listens on port 8090 when launched with `server --port 8090`.
-  # The ENTRYPOINT is `/app/bin/echidna`; CMD gets overridden below.
   RUST_LOG = "info"
   ECHIDNA_HOST = "[::]"
   ECHIDNA_PORT = "8090"
 
 [processes]
   app = "server --port 8090 --host [::] --cors"
 
-# Internal-only TCP on :8090
-[[services]]
-  protocol = "tcp"
+# Public HTTPS — terminates TLS at the Fly edge, forwards to internal :8090.
+[http_service]
   internal_port = 8090
+  force_https = true
   auto_stop_machines = "stop"
   auto_start_machines = true
   min_machines_running = 0
   processes = ["app"]
-
-  [[services.ports]]
-    port = 8090
-    handlers = []
-
-  # HTTP check on /api/health — tests the server is serving, not just the port.
-  # grace_period must be generous: Isabelle Main heap maps ~1-2 GB on first load
-  # and Julia has JIT overhead on first prover call.  90s is the minimum safe value.
-  [[services.http_checks]]
+  [http_service.concurrency]
+    type = "requests"
+    hard_limit = 25
+    soft_limit = 20
+
+  # Grace period is generous: Isabelle Main heap maps ~1-2 GB on cold start;
+  # Julia has JIT overhead on first prover call.  90s is the minimum safe value.
+  [[http_service.checks]]
     interval = "30s"
     timeout = "10s"
     grace_period = "90s"
@@ -56,6 +55,6 @@ kill_timeout = "10s"
 
 [[vm]]
   size = "shared-cpu-2x"
-  memory = "4096mb"  # Julia + Agda + Isabelle Main heap need real RAM
+  memory = "4096mb"
   cpu_kind = "shared"
   cpus = 2