echidna/selur-compose.toml at main · hyperpolymath/echidna · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
# SPDX-License-Identifier: PMPL-1.0-or-later
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
#
# ECHIDNA — Stapeln/Selur service definition.
#
# Multi-stage Rust build with Z3 SMT solver + Lean 4 prover.
# Exposes HTTP API on port 8081 (GraphQL/gRPC/REST interfaces).
#
# Usage:
#   podman-compose -f selur-compose.toml up -d
#   just stack-up
#
# The Containerfile uses three build stages:
#   1. rust-builder      — Compiles echidna binary from Rust source
#   2. prover-installer  — Downloads Z3 4.13.4 + installs Lean 4 via elan
#   3. runtime           — Chainguard wolfi-base with binaries + provers

[project]
name = "echidna"

# =============================================================================
# ECHIDNA — Neurosymbolic theorem proving platform
# =============================================================================
[services.app]
build = { context = ".", dockerfile = "Containerfile" }
restart = "unless-stopped"
ports = ["8081:8081"]
networks = ["echidna-internal"]
environment = [
  "ECHIDNA_PROVER_PATH=/opt",
  "RUST_LOG=info",
]
volumes = [
  "echidna-proofs:/app/proofs",
  "echidna-config:/app/config",
  "echidna-logs:/app/logs",
]
healthcheck = { test = "/app/bin/echidna --version || exit 1", interval = "30s", timeout = "10s", retries = 3 }

# =============================================================================
# Networks
# =============================================================================
[networks.echidna-internal]
driver = "bridge"

# =============================================================================
# Volumes
# =============================================================================
[volumes.echidna-proofs]
driver = "local"

[volumes.echidna-config]
driver = "local"

[volumes.echidna-logs]
driver = "local"