Skip to content

Commit d3db97d

Browse files
refactor(l3/l1): consolidate Wave-3 to one Containerfile.wave3; ratify Zig-shim; Guix-primary (#73)
## What Reconciles long-standing stale-doc-drift and lands three ratified decisions. ### L3 Wave-3 — consolidated (the real inefficiency, fixed) The nine `.containerization/Containerfile.<backend>` files each re-compiled the entire Rust core (≈9× the same build). Replaced with **one multi-target `.containerization/Containerfile.wave3`**: a single shared `rust-builder` stage + one `--target` per prover. Per-backend runtime stages (deps/ENV/healthcheck) preserved verbatim — only the duplicated compile is removed. `Justfile` `container-build-*` recipes and the `container-ci.yml` Tier-3 matrix rewired to `-f Containerfile.wave3 --target <prover>`. Imandra target stays licence-gated. Guix-extend was investigated empirically and rejected as the primary path: only `scip`/`or-tools`/`metamath` are in Guix; 5 need bespoke package definitions; Imandra is non-free. ### Packaging — Guix primary + sealed-container escape (estate ruling 2026-05-18) `flake.nix` + `flake.lock` removed (a Nix file that only mirrors the Guix manifest is drift, not a fallback). `manifests/live-provers.scm`, `.claude/CLAUDE.md`, `Justfile`, `STATE.a2ml` reconciled. The sealed container (`Containerfile.wave3`) is the single escape hatch for the not-in-Guix / non-free tail. Estate-wide rollout tracked as tech debt in `hyperpolymath/standards`. ### L1 — Julia transport ratified Open question #2 resolved: **Zig C-ABI shim (buffer-oriented), not `CapnProto.jl`** (estate-canonical: FFI=Zig, one codec shared with Rust, Zig = interface-safety transaction layer). `L1-CAPNPROTO-PROMPT.md`, `VERSIONING.md`, `TODO.md` reconciled; ReScript binding line corrected to AffineScript (estate ban); fixed dangling `L1-CAPNPROTO.md` ref in `echidna.capnp`. ## Why now Wave-3 Containerfiles + L1 schemas were **already landed on main** (`a87fae1`/`0a78906`/`b2a2ff7`) while `TODO.md`/`STATE.a2ml` still said "author them". Verified by reading, not trusting status text. ## Scope / caveats - `Refs #53` — does **not** close any requirements-target issue. - Static-correctness only: full `podman build` of the 9 targets was **not** run in this environment (heavy). Stage graph validated by construction — all 9 target stages present, every `COPY --from=` resolves, `rust-builder` defined once and shared. - L1 *implementation* remains gated on the L3 hand-off (Tier-1 green ≥7d on main; main CI stuck `queued/`, infra-owned). This PR is spec/design + L3 consolidation only. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent f611277 commit d3db97d

24 files changed

Lines changed: 1151 additions & 1468 deletions

.claude/CLAUDE.md

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -134,8 +134,13 @@ package definitions (not metadata files) and must NOT be deleted.
134134

135135
### Package Management
136136

137-
- **Primary**: Guix (guix.scm)
138-
- **Fallback**: Nix (flake.nix)
137+
- **Primary**: Guix (`guix.scm`, `manifests/*.scm`)
138+
- **Escape hatch**: a sealed container (`.containerization/Containerfile.wave3`)
139+
for the not-in-Guix / non-free tail. **NO Nix mirror** — estate ruling
140+
2026-05-18 (Guix primary + sealed-container escape). `flake.nix` is
141+
deprecated and removed; a `flake.nix` that only mirrors the Guix manifest is
142+
drift, not a fallback. A second packager is permitted only where it is the
143+
sole source of a specific named dependency, documented as such.
139144
- **JS deps**: Deno (deno.json imports)
140145

141146
### Security Requirements

.containerization/Containerfile

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,8 +27,14 @@ RUN rustup toolchain install nightly && rustup default nightly
2727
WORKDIR /build
2828

2929
COPY Cargo.toml Cargo.lock ./
30+
# Workspace members: crates/* (echidna-core, -core-spark, -mcp, -wire,
31+
# typed_wasm) + src/interfaces/* + root pkg at src/rust. Omitting `crates/`
32+
# makes the rust-builder stage fail — the workspace manifest references
33+
# crates/echidna-core (matches Containerfile.wave3).
34+
COPY crates ./crates
3035
COPY src/rust ./src/rust
3136
COPY src/interfaces ./src/interfaces
37+
COPY benches ./benches
3238

3339
# Build release binary
3440
RUN cargo build --release --bin echidna

.containerization/Containerfile.acl2

Lines changed: 0 additions & 124 deletions
This file was deleted.

.containerization/Containerfile.full

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,11 @@ RUN rustup toolchain install nightly && rustup default nightly
2727
WORKDIR /build
2828

2929
COPY Cargo.toml Cargo.lock ./
30+
# Workspace members: crates/* (echidna-core, -core-spark, -mcp, -wire,
31+
# typed_wasm) + src/interfaces/* + root pkg at src/rust. Omitting `crates/`
32+
# makes the rust-builder stage fail — the workspace manifest references
33+
# crates/echidna-core (matches Containerfile.wave3).
34+
COPY crates ./crates
3035
COPY src/rust ./src/rust
3136
COPY src/interfaces ./src/interfaces
3237
COPY benches ./benches

.containerization/Containerfile.hol4

Lines changed: 0 additions & 157 deletions
This file was deleted.

0 commit comments

Comments
 (0)