Skip to content

Commit a87fae1

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(l3-wave3): complete Wave-3 Tier-3 container infrastructure (9 backends)
Add the missing Imandra gated stub Containerfile, weekly tier3-container CI matrix job (8 non-proprietary images, allow-fail, 90 min timeout for HOL4/ACL2), and Justfile recipes (container-build-tier3 + per-backend targets). Also fixes the stale v4 checkout SHA in container-ci.yml to the canonical v6.0.2 pin. STATE.a2ml updated to mark Wave-3 LANDED. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 45d1de0 commit a87fae1

4 files changed

Lines changed: 292 additions & 17 deletions

File tree

‎.containerization/Containerfile.imandra‎

Lines changed: 128 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,128 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
#
4+
# ECHIDNA Imandra Containerfile — GATED (proprietary licence required)
5+
# Build: podman build -f .containerization/Containerfile.imandra -t echidna:imandra .
6+
# Seal: selur seal echidna:imandra
7+
# Sign: cerro-torre sign echidna:imandra
8+
#
9+
# Imandra: an industrial theorem prover and program analyser for OCaml and
10+
# functional languages (Aesthetic Integration / Imandra Inc.).
11+
# Licence: proprietary — an Imandra account and signed licence agreement are
12+
# required before the binary can be downloaded.
13+
#
14+
# WHY THIS CONTAINERFILE IS GATED
15+
# ────────────────────────────────
16+
# Imandra does not publish a redistributable binary or source tarball.
17+
# Automated CI downloads require a bearer token from Imandra Inc. and an
18+
# active licence agreement. Building this image without a signed licence
19+
# is not permitted under Imandra's terms.
20+
#
21+
# HOW TO ENABLE
22+
# ─────────────
23+
# 1. Register at https://imandra.ai/ and accept the licence.
24+
# 2. Download the Imandra CLI installer: `bash -c "$(curl -fsSL https://storage.googleapis.com/imandra-do/install.sh)"`
25+
# 3. Log in: `imandra auth login`
26+
# 4. Obtain the installer token from `~/.imandra/token` after auth.
27+
# 5. Pass the token as a build ARG:
28+
# podman build \
29+
# --secret id=imandra_token,src=~/.imandra/token \
30+
# -f .containerization/Containerfile.imandra \
31+
# -t echidna:imandra .
32+
# 6. Remove the ECHO_UNSUPPORTED line from Stage 2 and un-comment
33+
# the curl-install block below.
34+
#
35+
# ECHIDNA uses the Imandra backend (ProverKind::Imandra) for OCaml program
36+
# verification and bounded model checking. In CI, the backend is mock-only
37+
# unless this image is built and available on the runner.
38+
39+
# =============================================================================
40+
# Stage 1: Rust Builder
41+
# =============================================================================
42+
FROM docker.io/library/rust:1.85-slim-bookworm AS rust-builder
43+
44+
RUN apt-get update && apt-get install -y --no-install-recommends \
45+
build-essential \
46+
pkg-config \
47+
libssl-dev \
48+
&& rm -rf /var/lib/apt/lists/*
49+
50+
RUN rustup toolchain install nightly && rustup default nightly
51+
52+
WORKDIR /build
53+
54+
COPY Cargo.toml Cargo.lock ./
55+
COPY src/rust ./src/rust
56+
COPY src/interfaces ./src/interfaces
57+
58+
RUN cargo build --release --bin echidna
59+
60+
# =============================================================================
61+
# Stage 2: Imandra Installer (PROPRIETARY — gated, replace block when licensed)
62+
# =============================================================================
63+
FROM docker.io/library/debian:bookworm-slim AS imandra-installer
64+
65+
RUN apt-get update && apt-get install -y --no-install-recommends \
66+
curl \
67+
ca-certificates \
68+
bash \
69+
&& rm -rf /var/lib/apt/lists/*
70+
71+
# ── GATE: emit stub and document the real install path ────────────────────────
72+
# Replace this block with the secret-mount curl install once a licence token
73+
# is available (see HOW TO ENABLE above).
74+
RUN mkdir -p /usr/local/bin && \
75+
printf '#!/bin/sh\necho "imandra: not available (proprietary licence required — see Containerfile.imandra)"\nexit 1\n' \
76+
> /usr/local/bin/imandra && \
77+
chmod +x /usr/local/bin/imandra
78+
79+
# ── REAL INSTALL (un-comment and fill in IMANDRA_TOKEN when licensed) ─────────
80+
# ARG IMANDRA_TOKEN
81+
# RUN --mount=type=secret,id=imandra_token,target=/run/secrets/imandra_token \
82+
# set -eux; \
83+
# TOKEN="$(cat /run/secrets/imandra_token)" && \
84+
# curl -fsSL \
85+
# -H "Authorization: Bearer ${TOKEN}" \
86+
# "https://storage.googleapis.com/imandra-do/install.sh" | bash && \
87+
# imandra --version
88+
# ────────────────────────────────────────────────────────────────────────────────
89+
90+
# =============================================================================
91+
# Stage 3: Runtime Image
92+
# =============================================================================
93+
FROM docker.io/library/debian:bookworm-slim
94+
95+
LABEL maintainer="Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"
96+
LABEL org.opencontainers.image.source="https://github.com/hyperpolymath/echidna"
97+
LABEL org.opencontainers.image.description="ECHIDNA + Imandra stub (proprietary licence required for real binary)"
98+
LABEL org.opencontainers.image.licenses="PMPL-1.0-or-later"
99+
LABEL org.opencontainers.image.version="2.3.0"
100+
LABEL org.opencontainers.image.vendor="hyperpolymath"
101+
102+
RUN apt-get update && apt-get install -y --no-install-recommends \
103+
ca-certificates \
104+
libssl3 \
105+
&& rm -rf /var/lib/apt/lists/*
106+
107+
WORKDIR /app
108+
109+
COPY --from=rust-builder /build/target/release/echidna /app/bin/echidna
110+
COPY --from=imandra-installer /usr/local/bin/imandra /usr/local/bin/imandra
111+
112+
ENV PATH="/app/bin:/usr/local/bin:${PATH}"
113+
ENV ECHIDNA_PROVER_PATH="/usr/local/bin"
114+
115+
RUN mkdir -p /app/proofs /app/config /app/logs
116+
117+
# REST API
118+
EXPOSE 8000
119+
# GraphQL
120+
EXPOSE 8081
121+
# gRPC
122+
EXPOSE 50051
123+
124+
HEALTHCHECK --interval=30s --timeout=10s --start-period=15s --retries=3 \
125+
CMD ["/app/bin/echidna", "--version"]
126+
127+
ENTRYPOINT ["/app/bin/echidna"]
128+
CMD ["--help"]

‎.github/workflows/container-ci.yml‎

Lines changed: 115 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,14 @@
11
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
#
3+
# container-ci.yml — Container build verification.
4+
#
5+
# Two jobs:
6+
# container-build — builds the minimal ECHIDNA image on every PR/push;
7+
# hard gate.
8+
# tier3-container — builds each Wave-3 prover image weekly (Sunday 06:00 UTC)
9+
# and on any change to the .containerization/** tree;
10+
# allow-fail per image (proprietary builds excluded).
11+
212
name: Container Build Verification
313

414
on:
@@ -18,15 +28,24 @@ on:
1828
- 'Cargo.lock'
1929
- 'src/rust/**'
2030
- '.github/workflows/container-ci.yml'
31+
schedule:
32+
# Weekly build of Tier-3 prover images (Sunday 06:00 UTC).
33+
# Distinct from live-provers.yml Tier-3 run (Sunday 05:00 UTC)
34+
# so the container build does not race the live-prover tests.
35+
- cron: '0 6 * * 0'
2136

22-
permissions: read-all
37+
permissions:
38+
contents: read
2339

2440
jobs:
41+
# ── Job 1: minimal image — hard gate on every PR/push ─────────────────────
2542
container-build:
2643
name: Build & verify container image
2744
runs-on: ubuntu-latest
45+
2846
steps:
29-
- uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
47+
- name: Checkout
48+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
3049

3150
- name: Install Podman
3251
run: |
@@ -44,35 +63,118 @@ jobs:
4463
- name: Verify image metadata
4564
run: |
4665
echo "=== Image labels ==="
47-
podman inspect echidna:ci-test --format '{{range $k, $v := .Config.Labels}}{{$k}}: {{$v}}{{"\n"}}{{end}}'
48-
66+
podman inspect echidna:ci-test \
67+
--format '{{range $k, $v := .Config.Labels}}{{$k}}: {{$v}}{{"\n"}}{{end}}'
4968
echo "=== Image size ==="
5069
podman images echidna:ci-test --format "{{.Size}}"
5170
5271
- name: Verify ECHIDNA binary runs
5372
run: |
5473
echo "=== echidna --version ==="
5574
podman run --rm echidna:ci-test --version
56-
5775
echo "=== echidna --help ==="
5876
podman run --rm echidna:ci-test --help
5977
6078
- name: Verify solver availability inside container
6179
run: |
6280
echo "=== Checking installed solvers ==="
6381
podman run --rm --entrypoint /bin/sh echidna:ci-test -c '
64-
echo "Z3:"; z3 --version 2>/dev/null || echo " not found"
65-
echo "Lean:"; lean --version 2>/dev/null || echo " not found"
82+
echo "Z3:"; z3 --version 2>/dev/null || echo " not found"
83+
echo "Lean:"; lean --version 2>/dev/null || echo " not found"
6684
echo "Idris2:"; idris2 --version 2>/dev/null || echo " not found"
6785
'
6886
69-
- name: Verify healthcheck
87+
- name: Clean up
88+
if: always()
89+
run: podman rmi echidna:ci-test 2>/dev/null || true
90+
91+
# ── Job 2: Wave-3 Tier-3 prover images — weekly, allow-fail per image ─────
92+
#
93+
# Runs on the weekly schedule and whenever any .containerization/** file
94+
# changes. Each prover builds in its own matrix cell; allow-fail is set
95+
# at cell level so one broken prover does not mask the others.
96+
#
97+
# Imandra is excluded: it is proprietary and requires a licence token not
98+
# available in public CI.
99+
tier3-container:
100+
name: Tier-3 / ${{ matrix.prover }}
101+
runs-on: ubuntu-latest
102+
# Run on schedule or when the .containerization tree changes on main.
103+
# Not a merge gate — these are informational weekly builds.
104+
if: >-
105+
github.event_name == 'schedule' ||
106+
(github.event_name == 'push' && contains(github.event.head_commit.modified, '.containerization/'))
107+
continue-on-error: true
108+
strategy:
109+
fail-fast: false
110+
matrix:
111+
include:
112+
- prover: tamarin
113+
image: echidna:tamarin
114+
file: .containerization/Containerfile.tamarin
115+
version_check: "tamarin-prover --version"
116+
- prover: proverif
117+
image: echidna:proverif
118+
file: .containerization/Containerfile.proverif
119+
version_check: "proverif -help 2>&1 | head -1"
120+
- prover: metamath
121+
image: echidna:metamath
122+
file: .containerization/Containerfile.metamath
123+
version_check: "echo exit | metamath 2>&1 | head -1 || true"
124+
- prover: twelf
125+
image: "echidna:twelf"
126+
file: .containerization/Containerfile.twelf
127+
version_check: "twelf-server --help 2>&1 | head -1 || true"
128+
- prover: or-tools
129+
image: echidna:or-tools
130+
file: .containerization/Containerfile.or-tools
131+
version_check: "ls /usr/local/lib/libortools* 2>/dev/null | head -1 || true"
132+
- prover: scip
133+
image: echidna:scip
134+
file: .containerization/Containerfile.scip
135+
version_check: "scip --version 2>&1 | head -1 || true"
136+
- prover: hol4
137+
image: echidna:hol4
138+
file: .containerization/Containerfile.hol4
139+
version_check: "echo '(* quit *);' | hol 2>&1 | head -1 || true"
140+
- prover: acl2
141+
image: echidna:acl2
142+
file: .containerization/Containerfile.acl2
143+
version_check: "echo '(acl2::quit)' | acl2 2>&1 | head -3 || true"
144+
145+
steps:
146+
- name: Checkout
147+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
148+
149+
- name: Install Podman
70150
run: |
71-
echo "=== Running healthcheck command ==="
72-
podman run --rm echidna:ci-test --version
73-
echo "✓ Healthcheck passed"
151+
sudo apt-get update -q
152+
sudo apt-get install -y -q podman
153+
154+
- name: Build ${{ matrix.prover }} image
155+
# HOL4 and ACL2 have long build times; give them extra headroom.
156+
timeout-minutes: 90
157+
run: |
158+
podman build \
159+
-f "${{ matrix.file }}" \
160+
-t "${{ matrix.image }}" \
161+
--no-cache \
162+
.
163+
164+
- name: Verify ECHIDNA binary inside ${{ matrix.prover }} image
165+
run: |
166+
podman run --rm "${{ matrix.image }}" --version
167+
168+
- name: Smoke-check ${{ matrix.prover }} binary
169+
run: |
170+
podman run --rm --entrypoint /bin/sh "${{ matrix.image }}" \
171+
-c '${{ matrix.version_check }}'
172+
173+
- name: Verify image metadata
174+
run: |
175+
podman inspect "${{ matrix.image }}" \
176+
--format '{{index .Config.Labels "org.opencontainers.image.description"}}'
74177
75178
- name: Clean up
76179
if: always()
77-
run: |
78-
podman rmi echidna:ci-test 2>/dev/null || true
180+
run: podman rmi "${{ matrix.image }}" 2>/dev/null || true

‎.machine_readable/6a2/STATE.a2ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -834,7 +834,7 @@ changes = [
834834
l3-status-after-wave-2 = [
835835
"Wave-1 (Tier-1, every PR, 9 backends): DONE — landed in b022bf4.",
836836
"Wave-2 (Tier-2, nightly, 10 backends): DONE for 9; hol-light deferred to Wave-3.",
837-
"Wave-3 (Tier-3, weekly, 9 backends: Tamarin, ProVerif, Imandra, SCIP, OR-Tools, HOL4, ACL2, Twelf, Metamath): Containerfiles present in .containerization/, tier3 matrix job wired in live-provers.yml. Imandra gated on licence. Others provision via apt/tarball with continue-on-error.",
837+
"Wave-3 (Tier-3, weekly, 9 backends: Tamarin, ProVerif, Imandra, SCIP, OR-Tools, HOL4, ACL2, Twelf, Metamath): LANDED. All 9 Containerfiles in .containerization/ (Imandra is proprietary-gated stub). Justfile: container-build-tier3 + per-backend recipes. container-ci.yml: weekly tier3-container matrix job, 8 non-proprietary images, allow-fail, 90 min timeout for HOL4/ACL2.",
838838
"Wave-4 (Tier-4, quarterly, 19 backends): SCAFFOLD ONLY — placeholder tier4 job in live-provers.yml announces list. See wave-4-rationale for per-backend mock-only justification.",
839839
]
840840
wave-4-rationale = {

‎Justfile‎

Lines changed: 48 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -443,6 +443,41 @@ container-build:
443443
container-build-full:
444444
podman build -f .containerization/Containerfile.full -t echidna:full .
445445

446+
# ── Tier-3 prover containers (Wave-3) ────────────────────────────────────────
447+
448+
# Build all non-proprietary Tier-3 prover containers (skip imandra — licence required)
449+
container-build-tier3: container-build-tamarin container-build-proverif container-build-metamath \
450+
container-build-twelf container-build-or-tools container-build-scip \
451+
container-build-hol4 container-build-acl2
452+
453+
container-build-tamarin:
454+
podman build -f .containerization/Containerfile.tamarin -t echidna:tamarin .
455+
456+
container-build-proverif:
457+
podman build -f .containerization/Containerfile.proverif -t echidna:proverif .
458+
459+
container-build-metamath:
460+
podman build -f .containerization/Containerfile.metamath -t echidna:metamath .
461+
462+
container-build-twelf:
463+
podman build -f .containerization/Containerfile.twelf -t echidna:twelf .
464+
465+
container-build-or-tools:
466+
podman build -f .containerization/Containerfile.or-tools -t echidna:or-tools .
467+
468+
container-build-scip:
469+
podman build -f .containerization/Containerfile.scip -t echidna:scip .
470+
471+
container-build-hol4:
472+
podman build -f .containerization/Containerfile.hol4 -t echidna:hol4 .
473+
474+
container-build-acl2:
475+
podman build -f .containerization/Containerfile.acl2 -t echidna:acl2 .
476+
477+
# Build imandra stub (proprietary; real binary requires a signed licence — see Containerfile.imandra)
478+
container-build-imandra:
479+
podman build -f .containerization/Containerfile.imandra -t echidna:imandra .
480+
446481
# Run echidna container
447482
container-run *ARGS:
448483
podman run --rm -it echidna:latest {{ARGS}}
@@ -755,9 +790,19 @@ help-me:
755790
echo " just run prove <f> - Prove a file"
756791
echo ""
757792
echo "Containers:"
758-
echo " just container-build - Minimal image"
759-
echo " just container-build-full - Full image (all provers)"
760-
echo " just container-run - Run container"
793+
echo " just container-build - Minimal image"
794+
echo " just container-build-full - Full image (all provers)"
795+
echo " just container-build-tier3 - All Wave-3 prover images (except imandra)"
796+
echo " just container-build-tamarin - Tamarin security protocol prover"
797+
echo " just container-build-proverif - ProVerif cryptographic protocol verifier"
798+
echo " just container-build-metamath - Metamath (pure-Rust in-process + bundled databases)"
799+
echo " just container-build-twelf - Twelf LF meta-logical framework"
800+
echo " just container-build-or-tools - OR-Tools combinatorial optimisation C++ library"
801+
echo " just container-build-scip - SCIP constraint integer programming solver"
802+
echo " just container-build-hol4 - HOL4 (Poly/ML build, slow)"
803+
echo " just container-build-acl2 - ACL2 (SBCL build, slow)"
804+
echo " just container-build-imandra - Imandra stub (proprietary licence required)"
805+
echo " just container-run - Run container"
761806
echo ""
762807
echo "Chapel accelerator:"
763808
echo " just chapel-all - Build + test Chapel layer"

0 commit comments

Comments
 (0)