Skip to content

Commit 7be0efb

Browse files
hyperpolymathclaude
andcommitted
feat(chapel): Enable Chapel accelerator build integration
Wire up the dormant Chapel parallel proof search into the build system: - Add `chapel` feature flag to Cargo.toml - Add build.rs to link Zig FFI library when feature enabled - Update build.zig for Zig 0.14+/0.15+ API compatibility - Add C header (chapel_ffi_exports.h) defining Chapel ↔ Zig ABI - Add stub implementations for building/testing without Chapel runtime - Add Justfile recipes (build-chapel-ffi, test-chapel, chapel-all, etc.) - Add chapel-ci.yml workflow (Zig FFI build + Rust feature gate CI) - Fix var→const in chapel_bridge.zig for Zig 0.15 compliance The Chapel accelerator remains optional (default off). Enable with: just build-chapel # or: cargo build --features chapel Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 2be1e5c commit 7be0efb

8 files changed

Lines changed: 286 additions & 36 deletions

File tree

.github/workflows/chapel-ci.yml

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
name: Chapel Accelerator CI
3+
4+
on:
5+
push:
6+
paths:
7+
- 'src/zig_ffi/**'
8+
- 'src/rust/proof_search.rs'
9+
- 'chapel_poc/**'
10+
- 'Cargo.toml'
11+
- '.github/workflows/chapel-ci.yml'
12+
pull_request:
13+
paths:
14+
- 'src/zig_ffi/**'
15+
- 'src/rust/proof_search.rs'
16+
- 'chapel_poc/**'
17+
- 'Cargo.toml'
18+
- '.github/workflows/chapel-ci.yml'
19+
20+
permissions: read-all
21+
22+
jobs:
23+
zig-ffi:
24+
name: Build & Test Zig FFI Bridge
25+
runs-on: ubuntu-latest
26+
steps:
27+
- uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
28+
29+
- name: Install Zig
30+
uses: goto-bus-stop/setup-zig@7ab2955eb728f5440978d7e4f60155e5e3a9e02f # v2
31+
with:
32+
version: 0.13.0
33+
34+
- name: Build Zig FFI library
35+
run: cd src/zig_ffi && zig build -Doptimize=ReleaseSafe
36+
37+
- name: Run Zig FFI tests
38+
run: cd src/zig_ffi && zig build test
39+
40+
- name: Upload FFI library artifact
41+
uses: actions/upload-artifact@b4b15b8c7c6ac21ea08fcf65892d2ee8f75cf882 # v4
42+
with:
43+
name: chapel-ffi-lib
44+
path: src/zig_ffi/zig-out/lib/
45+
46+
rust-chapel-feature:
47+
name: Rust Build with Chapel Feature
48+
runs-on: ubuntu-latest
49+
needs: zig-ffi
50+
steps:
51+
- uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
52+
53+
- name: Install Rust toolchain
54+
uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable
55+
with:
56+
toolchain: stable
57+
58+
- name: Rust cache
59+
uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2
60+
61+
- name: Download FFI library
62+
uses: actions/download-artifact@fa0a91b85d4f404e444e00e005971372dc801d16 # v4
63+
with:
64+
name: chapel-ffi-lib
65+
path: src/zig_ffi/zig-out/lib/
66+
67+
- name: Build with chapel feature
68+
run: cargo build --features chapel
69+
70+
- name: Test with chapel feature
71+
run: cargo test --features chapel -- proof_search

Cargo.toml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -69,6 +69,10 @@ lazy_static = "1"
6969
# Chrono for timestamps
7070
chrono = { version = "0.4", features = ["serde"] }
7171

72+
[features]
73+
default = []
74+
chapel = [] # Enable Chapel parallel proof search (requires Zig FFI library)
75+
7276
[dev-dependencies]
7377
proptest = "1"
7478
tempfile = "3"

Justfile

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -96,6 +96,42 @@ container-build-full:
9696
container-run *ARGS:
9797
podman run --rm -it echidna:latest {{ARGS}}
9898

99+
# ── Chapel Accelerator ──────────────────────────────────────
100+
101+
# Build Zig FFI bridge for Chapel (prerequisite for --features chapel)
102+
build-chapel-ffi:
103+
@echo "Building Zig FFI bridge..."
104+
cd src/zig_ffi && zig build -Doptimize=ReleaseSafe
105+
@echo "Library built at src/zig_ffi/zig-out/lib/"
106+
107+
# Build Chapel PoC (requires Chapel compiler)
108+
build-chapel-poc:
109+
@echo "Building Chapel proof-of-concept..."
110+
cd chapel_poc && chpl parallel_proof_search.chpl -o proof_search --fast
111+
@echo "Built chapel_poc/proof_search"
112+
113+
# Run Chapel PoC benchmark
114+
run-chapel-poc:
115+
cd chapel_poc && ./proof_search
116+
117+
# Build with Chapel support enabled (requires Zig FFI built first)
118+
build-chapel: build-chapel-ffi
119+
cargo build --features chapel
120+
121+
# Test Chapel integration
122+
test-chapel: build-chapel-ffi
123+
cargo test --features chapel -- proof_search
124+
125+
# Test Zig FFI bridge independently
126+
test-chapel-ffi:
127+
cd src/zig_ffi && zig build test
128+
129+
# Full Chapel build + test
130+
chapel-all: build-chapel-poc build-chapel-ffi test-chapel
131+
@echo "Chapel accelerator fully built and tested"
132+
133+
# ── Other ───────────────────────────────────────────────────
134+
99135
# [AUTO-GENERATED] Multi-arch / RISC-V target
100136
build-riscv:
101137
@echo "Building for RISC-V..."

build.rs

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
//! Build script for ECHIDNA
3+
//!
4+
//! When the `chapel` feature is enabled, this links against the Zig-built
5+
//! Chapel FFI bridge library (libechidna_chapel_ffi).
6+
//!
7+
//! Build order: Chapel (.chpl) → C headers → Zig (chapel_bridge.zig) → Rust (proof_search.rs)
8+
9+
fn main() {
10+
// Only link Chapel FFI when the feature is enabled
11+
#[cfg(feature = "chapel")]
12+
{
13+
// Look for the Zig-built library in src/zig_ffi/zig-out/lib/
14+
let zig_ffi_dir = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR"))
15+
.join("src")
16+
.join("zig_ffi")
17+
.join("zig-out")
18+
.join("lib");
19+
20+
if zig_ffi_dir.exists() {
21+
println!("cargo:rustc-link-search=native={}", zig_ffi_dir.display());
22+
println!("cargo:rustc-link-lib=static=echidna_chapel_ffi");
23+
println!("cargo:rustc-link-lib=dylib=c");
24+
} else {
25+
// Also check standard install location
26+
let alt_dir = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR"))
27+
.join("lib");
28+
if alt_dir.exists() {
29+
println!("cargo:rustc-link-search=native={}", alt_dir.display());
30+
println!("cargo:rustc-link-lib=static=echidna_chapel_ffi");
31+
println!("cargo:rustc-link-lib=dylib=c");
32+
} else {
33+
println!("cargo:warning=Chapel FFI library not found. Build it first with: just build-chapel-ffi");
34+
println!("cargo:warning=Looked in: {}", zig_ffi_dir.display());
35+
}
36+
}
37+
38+
// Re-run if FFI source changes
39+
println!("cargo:rerun-if-changed=src/zig_ffi/chapel_bridge.zig");
40+
println!("cargo:rerun-if-changed=src/zig_ffi/build.zig");
41+
}
42+
}

src/zig_ffi/build.zig

Lines changed: 29 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
// SPDX-License-Identifier: PMPL-1.0-or-later
22
// ECHIDNA Zig FFI Build Configuration
3+
// Compatible with Zig 0.14+/0.15+
34

45
const std = @import("std");
56

@@ -8,58 +9,51 @@ pub fn build(b: *std.Build) void {
89
const optimize = b.standardOptimizeOption(.{});
910

1011
// Build shared library for FFI
11-
const lib = b.addSharedLibrary(.{
12+
const lib = b.addLibrary(.{
1213
.name = "echidna_chapel_ffi",
13-
.root_source_file = b.path("chapel_bridge.zig"),
14-
.target = target,
15-
.optimize = optimize,
14+
.root_module = b.createModule(.{
15+
.root_source_file = b.path("chapel_bridge.zig"),
16+
.target = target,
17+
.optimize = optimize,
18+
.link_libc = true,
19+
}),
20+
.linkage = .dynamic,
1621
});
17-
18-
// Link with C (required for Chapel interop)
19-
lib.linkLibC();
20-
21-
// Set version
22-
lib.version = .{ .major = 1, .minor = 0, .patch = 0 };
22+
// Chapel C headers are in the same directory
23+
lib.root_module.addIncludePath(b.path("."));
2324

2425
// Install artifacts
2526
b.installArtifact(lib);
2627

2728
// Static library (alternative)
28-
const lib_static = b.addStaticLibrary(.{
29+
const lib_static = b.addLibrary(.{
2930
.name = "echidna_chapel_ffi",
30-
.root_source_file = b.path("chapel_bridge.zig"),
31-
.target = target,
32-
.optimize = optimize,
31+
.root_module = b.createModule(.{
32+
.root_source_file = b.path("chapel_bridge.zig"),
33+
.target = target,
34+
.optimize = optimize,
35+
.link_libc = true,
36+
}),
37+
.linkage = .static,
3338
});
39+
lib_static.root_module.addIncludePath(b.path("."));
3440

35-
lib_static.linkLibC();
3641
b.installArtifact(lib_static);
3742

38-
// Unit tests
43+
// Unit tests (link against stubs when Chapel not available)
3944
const lib_tests = b.addTest(.{
40-
.root_source_file = b.path("chapel_bridge.zig"),
41-
.target = target,
42-
.optimize = optimize,
45+
.root_module = b.createModule(.{
46+
.root_source_file = b.path("chapel_bridge.zig"),
47+
.target = target,
48+
.optimize = optimize,
49+
.link_libc = true,
50+
}),
4351
});
44-
45-
lib_tests.linkLibC();
52+
lib_tests.root_module.addIncludePath(b.path("."));
53+
lib_tests.addCSourceFile(.{ .file = b.path("chapel_stubs.c") });
4654

4755
const run_lib_tests = b.addRunArtifact(lib_tests);
4856

4957
const test_step = b.step("test", "Run FFI tests");
5058
test_step.dependOn(&run_lib_tests.step);
51-
52-
// Documentation
53-
const docs = b.addTest(.{
54-
.root_source_file = b.path("chapel_bridge.zig"),
55-
.target = target,
56-
.optimize = .Debug,
57-
});
58-
59-
const docs_step = b.step("docs", "Generate documentation");
60-
docs_step.dependOn(&b.addInstallDirectory(.{
61-
.source_dir = docs.getEmittedDocs(),
62-
.install_dir = .prefix,
63-
.install_subdir = "docs",
64-
}).step);
6559
}

src/zig_ffi/chapel_bridge.zig

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -214,7 +214,7 @@ pub fn parallelProofSearch(
214214
);
215215

216216
// Convert Chapel result to Zig (takes ownership of strings)
217-
var result = try ProofResult.fromChapel(c_result, allocator);
217+
const result = try ProofResult.fromChapel(c_result, allocator);
218218

219219
// Free Chapel-allocated strings (we've copied them)
220220
chapel.chapel_free_result(@constCast(&c_result));

src/zig_ffi/chapel_ffi_exports.h

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
/* SPDX-License-Identifier: PMPL-1.0-or-later */
2+
/* ECHIDNA Chapel FFI Exports — C header interface
3+
*
4+
* This header defines the C ABI that Chapel's `export` functions provide.
5+
* When Chapel is compiled, it generates compatible symbols.
6+
* When Chapel is NOT available, stub implementations return "unavailable".
7+
*
8+
* The Zig bridge (@cImport) imports this header and wraps it type-safely.
9+
*/
10+
11+
#ifndef ECHIDNA_CHAPEL_FFI_EXPORTS_H
12+
#define ECHIDNA_CHAPEL_FFI_EXPORTS_H
13+
14+
#include <stdint.h>
15+
16+
#ifdef __cplusplus
17+
extern "C" {
18+
#endif
19+
20+
/* C-compatible proof result from Chapel's parallel search */
21+
typedef struct {
22+
int success; /* 0 = false, 1 = true */
23+
int prover_id; /* ProverKind enum value (-1 if unknown) */
24+
double time_seconds;
25+
uint32_t tactic_count;
26+
const char *prover_name; /* NULL or heap-allocated string */
27+
const char *error_message; /* NULL or heap-allocated string */
28+
} CProofResult;
29+
30+
/* Main entry point: parallel proof search across all Chapel-managed provers.
31+
* goal: null-terminated theorem statement
32+
* prover_ids: array of prover IDs to use (NULL = all provers)
33+
* num_provers: length of prover_ids (0 = all provers)
34+
* Returns: CProofResult (caller must free via chapel_free_result) */
35+
CProofResult chapel_parallel_search(
36+
const char *goal,
37+
const int *prover_ids,
38+
int num_provers
39+
);
40+
41+
/* Free a CProofResult returned by chapel_parallel_search */
42+
void chapel_free_result(CProofResult *result);
43+
44+
/* Check if Chapel runtime is available (returns 1 if yes, 0 if no) */
45+
int chapel_is_available(void);
46+
47+
/* Get Chapel metalayer version string (caller must free via chapel_free_string) */
48+
const char *chapel_get_version(void);
49+
50+
/* Free a string returned by chapel_get_version */
51+
void chapel_free_string(const char *str);
52+
53+
#ifdef __cplusplus
54+
}
55+
#endif
56+
57+
#endif /* ECHIDNA_CHAPEL_FFI_EXPORTS_H */

src/zig_ffi/chapel_stubs.c

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
/* SPDX-License-Identifier: PMPL-1.0-or-later */
2+
/* Stub implementations of Chapel FFI exports for testing/building
3+
* without the Chapel runtime. These return "unavailable" gracefully. */
4+
5+
#include "chapel_ffi_exports.h"
6+
#include <stdlib.h>
7+
#include <string.h>
8+
9+
CProofResult chapel_parallel_search(
10+
const char *goal,
11+
const int *prover_ids,
12+
int num_provers
13+
) {
14+
(void)goal;
15+
(void)prover_ids;
16+
(void)num_provers;
17+
CProofResult result = {0};
18+
result.success = 0;
19+
result.prover_id = -1;
20+
result.time_seconds = 0.0;
21+
result.tactic_count = 0;
22+
result.prover_name = NULL;
23+
result.error_message = strdup("Chapel runtime not available (stub)");
24+
return result;
25+
}
26+
27+
void chapel_free_result(CProofResult *result) {
28+
if (result) {
29+
free((void *)result->prover_name);
30+
free((void *)result->error_message);
31+
result->prover_name = NULL;
32+
result->error_message = NULL;
33+
}
34+
}
35+
36+
int chapel_is_available(void) {
37+
return 0; /* Not available in stub mode */
38+
}
39+
40+
const char *chapel_get_version(void) {
41+
return NULL; /* No version in stub mode */
42+
}
43+
44+
void chapel_free_string(const char *str) {
45+
free((void *)str);
46+
}

0 commit comments

Comments
 (0)