Skip to content

Commit 0a78906

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(l1/l2/l3): Cap'n Proto IPC scaffold, Chapel parallel endpoint, Wave-3 Containerfiles
L1 — Cap'n Proto IPC (wave 0 scaffold): - schemas/echidna.capnp: full wire schema (ProofGoal, ProofResult, GnnRank*, ProofGraph, AxiomReport, TrustedOutcome, ProverInvocation, KeyValue; OutcomeTag/DispatchStrategy enums; all 7 NodeKind + 8 EdgeKind values) - src/rust/ipc/mod.rs: Transport enum (UDS primary / TCP fallback), from_env() correctly defaults to UDS, probe(), IpcClient stub with gnn_rank() returning Err until capnp-gen bindings land (L1 wave 1) - src/rust/lib.rs: pub mod ipc registered L2 — Chapel parallel dispatch endpoint: - src/rust/server.rs: /api/verify_parallel handler wired to ProverDispatcher::verify_proof_parallel (was dead code before) L3 — Wave-3 Containerfiles (8 prover backends): - .containerization/Containerfile.{tamarin,proverif,scip,or-tools, hol4,acl2,twelf,metamath} (Imandra skipped — proprietary, no public image) 685/685 lib tests passing, 0 clippy warnings on new code. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent b2dc327 commit 0a78906

12 files changed

Lines changed: 1398 additions & 0 deletions

‎.containerization/Containerfile.acl2‎

Lines changed: 124 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,124 @@
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 ACL2 Containerfile
5+
# Build: podman build -f .containerization/Containerfile.acl2 -t echidna:acl2 .
6+
# Seal: selur seal echidna:acl2
7+
# Sign: cerro-torre sign echidna:acl2
8+
#
9+
# ACL2: A Computational Logic for Applicative Common Lisp.
10+
# Industrial-strength theorem prover used in hardware verification (AMD, Intel).
11+
# Strategy: use SBCL (Steel Bank Common Lisp) prebuilt Debian package + build
12+
# ACL2 from source (acl2/acl2 on GitHub). The ACL2 build compiles itself
13+
# into a saved image using SBCL.
14+
# Build time: ~20-40 min.
15+
# Binary: acl2 (shell wrapper script created by the build process)
16+
17+
# =============================================================================
18+
# Stage 1: Rust Builder
19+
# =============================================================================
20+
FROM docker.io/library/rust:1.85-slim-bookworm AS rust-builder
21+
22+
RUN apt-get update && apt-get install -y --no-install-recommends \
23+
build-essential \
24+
pkg-config \
25+
libssl-dev \
26+
&& rm -rf /var/lib/apt/lists/*
27+
28+
RUN rustup toolchain install nightly && rustup default nightly
29+
30+
WORKDIR /build
31+
32+
COPY Cargo.toml Cargo.lock ./
33+
COPY src/rust ./src/rust
34+
COPY src/interfaces ./src/interfaces
35+
36+
RUN cargo build --release --bin echidna
37+
38+
# =============================================================================
39+
# Stage 2: ACL2 Builder (SBCL + ACL2 from source)
40+
# =============================================================================
41+
FROM docker.io/library/debian:bookworm-slim AS acl2-builder
42+
43+
RUN apt-get update && apt-get install -y --no-install-recommends \
44+
sbcl \
45+
curl \
46+
ca-certificates \
47+
git \
48+
build-essential \
49+
make \
50+
# ACL2 uses a small amount of C for foreign-call support
51+
gcc \
52+
&& rm -rf /var/lib/apt/lists/*
53+
54+
WORKDIR /build
55+
56+
# Clone ACL2 from the official GitHub mirror.
57+
# Use a versioned tag for reproducibility.
58+
# Check https://github.com/acl2/acl2/releases for the latest version.
59+
ARG ACL2_VERSION="8.6"
60+
RUN git clone --depth 1 --branch "v${ACL2_VERSION}" \
61+
https://github.com/acl2/acl2.git /build/acl2 \
62+
|| git clone --depth 1 \
63+
https://github.com/acl2/acl2.git /build/acl2
64+
65+
WORKDIR /build/acl2
66+
67+
# Build ACL2 using SBCL. The `make` target `LISP=sbcl` compiles ACL2 and
68+
# saves a SBCL core image. The resulting saved_acl2 is the executable image.
69+
RUN make LISP=sbcl -j"$(nproc)" \
70+
&& test -f /build/acl2/saved_acl2 \
71+
&& echo "ACL2 build succeeded"
72+
73+
# Create the acl2 wrapper script (mirrors the standard install convention)
74+
RUN printf '#!/bin/sh\nexec /opt/acl2/saved_acl2 "$@"\n' > /usr/local/bin/acl2 \
75+
&& chmod +x /usr/local/bin/acl2
76+
77+
# =============================================================================
78+
# Stage 3: Runtime Image
79+
# =============================================================================
80+
FROM docker.io/library/debian:bookworm-slim
81+
82+
LABEL maintainer="Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"
83+
LABEL org.opencontainers.image.source="https://github.com/hyperpolymath/echidna"
84+
LABEL org.opencontainers.image.description="ECHIDNA + ACL2 - applicative Common Lisp logic prover"
85+
LABEL org.opencontainers.image.licenses="PMPL-1.0-or-later"
86+
LABEL org.opencontainers.image.version="2.3.0"
87+
LABEL org.opencontainers.image.vendor="hyperpolymath"
88+
89+
# ACL2 at runtime runs a saved SBCL core image; only SBCL's C runtime is needed.
90+
RUN apt-get update && apt-get install -y --no-install-recommends \
91+
ca-certificates \
92+
libssl3 \
93+
sbcl \
94+
&& rm -rf /var/lib/apt/lists/*
95+
96+
WORKDIR /app
97+
98+
COPY --from=rust-builder /build/target/release/echidna /app/bin/echidna
99+
100+
# Copy ACL2 saved image and source tree (ACL2 loads books from its source tree)
101+
COPY --from=acl2-builder /build/acl2 /opt/acl2
102+
103+
# Install the acl2 wrapper script
104+
RUN printf '#!/bin/sh\nexec /opt/acl2/saved_acl2 "$@"\n' > /usr/local/bin/acl2 \
105+
&& chmod +x /usr/local/bin/acl2
106+
107+
ENV PATH="/app/bin:/usr/local/bin:${PATH}"
108+
ENV ACL2_SYSTEM_BOOKS="/opt/acl2/books"
109+
ENV ECHIDNA_PROVER_PATH="/usr/local/bin"
110+
111+
RUN mkdir -p /app/proofs /app/config /app/logs
112+
113+
# REST API
114+
EXPOSE 8000
115+
# GraphQL
116+
EXPOSE 8081
117+
# gRPC
118+
EXPOSE 50051
119+
120+
HEALTHCHECK --interval=30s --timeout=15s --start-period=30s --retries=3 \
121+
CMD ["/app/bin/echidna", "--version"]
122+
123+
ENTRYPOINT ["/app/bin/echidna"]
124+
CMD ["--help"]

‎.containerization/Containerfile.hol4‎

Lines changed: 157 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,157 @@
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 HOL4 Containerfile
5+
# Build: podman build -f .containerization/Containerfile.hol4 -t echidna:hol4 .
6+
# Seal: selur seal echidna:hol4
7+
# Sign: cerro-torre sign echidna:hol4
8+
#
9+
# HOL4: Higher-Order Logic theorem prover, successor to HOL88/HOL90.
10+
# Strategy: build from source using Poly/ML (Standard ML implementation).
11+
# Build time: ~30-60 min on 4 cores; needs ~4 GB RAM at peak.
12+
# Use BuildKit / Podman layer caching aggressively — the HOL4 source checkout
13+
# and Poly/ML build layers are stable and rarely change.
14+
# Binary: hol (shell wrapper in HOL4/bin/hol)
15+
16+
# =============================================================================
17+
# Stage 1: Rust Builder
18+
# =============================================================================
19+
FROM docker.io/library/rust:1.85-slim-bookworm AS rust-builder
20+
21+
RUN apt-get update && apt-get install -y --no-install-recommends \
22+
build-essential \
23+
pkg-config \
24+
libssl-dev \
25+
&& rm -rf /var/lib/apt/lists/*
26+
27+
RUN rustup toolchain install nightly && rustup default nightly
28+
29+
WORKDIR /build
30+
31+
COPY Cargo.toml Cargo.lock ./
32+
COPY src/rust ./src/rust
33+
COPY src/interfaces ./src/interfaces
34+
35+
RUN cargo build --release --bin echidna
36+
37+
# =============================================================================
38+
# Stage 2a: Poly/ML Builder
39+
# HOL4 requires Poly/ML >= 5.9; bookworm ships 5.9, which works but 5.10+ is
40+
# preferred. We build 5.9 from the Debian package for speed; upgrade the ARG
41+
# below to build from source if a newer version is needed.
42+
# =============================================================================
43+
FROM docker.io/library/debian:bookworm-slim AS polyml-builder
44+
45+
# BuildKit cache hint: Poly/ML sources change rarely — cache this layer hard.
46+
RUN apt-get update && apt-get install -y --no-install-recommends \
47+
build-essential \
48+
curl \
49+
ca-certificates \
50+
git \
51+
libgmp-dev \
52+
# Poly/ML build dependencies
53+
libffi-dev \
54+
&& rm -rf /var/lib/apt/lists/*
55+
56+
WORKDIR /build/polyml
57+
58+
# Download and build Poly/ML from source.
59+
# Poly/ML 5.9.1 is the latest stable release known to work with HOL4.
60+
ARG POLYML_VERSION="5.9.1"
61+
RUN curl -fsSL --retry 3 \
62+
"https://github.com/polyml/polyml/releases/download/v${POLYML_VERSION}/polyml-${POLYML_VERSION}.tar.gz" \
63+
-o /tmp/polyml.tar.gz \
64+
&& tar -xzf /tmp/polyml.tar.gz -C /build/polyml --strip-components=1 \
65+
&& rm /tmp/polyml.tar.gz
66+
67+
RUN ./configure --prefix=/opt/polyml \
68+
&& make -j"$(nproc)" \
69+
&& make install \
70+
&& /opt/polyml/bin/poly --version
71+
72+
# =============================================================================
73+
# Stage 2b: HOL4 Builder
74+
# Long build — runs `poly < tools/smart-configure.sml` then `bin/build`.
75+
# Layer caching on the git clone keeps re-builds fast when only HOL4 changes.
76+
# =============================================================================
77+
FROM docker.io/library/debian:bookworm-slim AS hol4-builder
78+
79+
RUN apt-get update && apt-get install -y --no-install-recommends \
80+
build-essential \
81+
git \
82+
ca-certificates \
83+
libgmp10 \
84+
&& rm -rf /var/lib/apt/lists/*
85+
86+
# Copy Poly/ML installation
87+
COPY --from=polyml-builder /opt/polyml /opt/polyml
88+
89+
ENV PATH="/opt/polyml/bin:${PATH}"
90+
91+
WORKDIR /build
92+
93+
# Clone HOL4; use a pinned commit tag for reproducibility.
94+
# Check https://github.com/HOL-Theorem-Prover/HOL/releases for latest.
95+
ARG HOL4_VERSION="kananaskis-15"
96+
RUN git clone --depth 1 --branch "${HOL4_VERSION}" \
97+
https://github.com/HOL-Theorem-Prover/HOL.git /build/HOL4
98+
99+
WORKDIR /build/HOL4
100+
101+
# Configure HOL4 against the Poly/ML we just built, then build all theories.
102+
# The smart-configure step auto-detects poly. The `bin/build` step compiles
103+
# the core theories (takes ~30-60 min on 4 vCPUs).
104+
RUN poly < tools/smart-configure.sml \
105+
&& bin/build
106+
107+
# Verify hol wrapper script exists
108+
RUN test -f /build/HOL4/bin/hol && echo "HOL4 build succeeded"
109+
110+
# =============================================================================
111+
# Stage 3: Runtime Image
112+
# =============================================================================
113+
FROM docker.io/library/debian:bookworm-slim
114+
115+
LABEL maintainer="Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"
116+
LABEL org.opencontainers.image.source="https://github.com/hyperpolymath/echidna"
117+
LABEL org.opencontainers.image.description="ECHIDNA + HOL4 - higher-order logic theorem prover"
118+
LABEL org.opencontainers.image.licenses="PMPL-1.0-or-later"
119+
LABEL org.opencontainers.image.version="2.3.0"
120+
LABEL org.opencontainers.image.vendor="hyperpolymath"
121+
122+
RUN apt-get update && apt-get install -y --no-install-recommends \
123+
ca-certificates \
124+
libssl3 \
125+
libgmp10 \
126+
libffi8 \
127+
&& rm -rf /var/lib/apt/lists/*
128+
129+
WORKDIR /app
130+
131+
COPY --from=rust-builder /build/target/release/echidna /app/bin/echidna
132+
133+
# Copy Poly/ML runtime (HOL4 loads ML code via poly at runtime)
134+
COPY --from=polyml-builder /opt/polyml /opt/polyml
135+
136+
# Copy HOL4 installation (includes pre-built heap images)
137+
COPY --from=hol4-builder /build/HOL4 /opt/HOL4
138+
139+
ENV PATH="/app/bin:/opt/polyml/bin:/opt/HOL4/bin:${PATH}"
140+
ENV HOLDIR="/opt/HOL4"
141+
ENV ECHIDNA_PROVER_PATH="/opt/HOL4/bin"
142+
143+
RUN mkdir -p /app/proofs /app/config /app/logs
144+
145+
# REST API
146+
EXPOSE 8000
147+
# GraphQL
148+
EXPOSE 8081
149+
# gRPC
150+
EXPOSE 50051
151+
152+
# HOL4 cold-start is slow (loads heap image); give generous start-period.
153+
HEALTHCHECK --interval=30s --timeout=15s --start-period=120s --retries=3 \
154+
CMD ["/app/bin/echidna", "--version"]
155+
156+
ENTRYPOINT ["/app/bin/echidna"]
157+
CMD ["--help"]

0 commit comments

Comments
 (0)