Skip to content

Commit cbd9449

Browse files
hyperpolymathclaude
andcommitted
feat(coprocessor): Phase 2a — FLINT FFI CAS backend
Adds `CoprocessorKind::FlintMath` and the full `FlintMathBackend` wired via Rust FFI to the FLINT C library (LGPL-3). FLINT is the only CAS backend in ECHIDNA that links in-process rather than shelling out — earning trust tier LibraryWrapped (Tier 3), same as `MathBackend`. ## What lands **New `CoprocessorOp` variants** (polynomial algebra + enhanced integer ops): - `FlintPolyGcd` — primitive GCD of two polynomials over Z - `FlintPolyMul` — product of two polynomials over Z - `FlintPolyRem` — pseudo-remainder (lc(g)^d · f = q·g + r) - `FlintPolyContent` — GCD of all coefficients of a polynomial - `FlintNthRoot` — exact integer k-th root (Empty if not exact) - `FlintBinomial` — binomial coefficient C(n, k) **New `CoprocessorOutcome::Polynomial`** — wire format: space-separated decimal coefficients in degree-ascending order; "0" for zero polynomial. **`src/rust/coprocessor/flint.rs`** — RAII wrappers (`Fmpz`, `FmpzPoly`) over `fmpz_t` / `fmpz_poly_t`; `extern "C"` declarations for 15 FLINT functions; `FlintMathBackend` implementing `Coprocessor`; 8 unit tests. **`--features flint`** — build.rs discovers system FLINT via pkg-config or bare `-lflint`. Without the feature, `CoprocessorFactory::native` returns `None` for `FlintMath` — callers fall through gracefully. **`julia_bridge.rs`** — exhaustive `kind_name` match extended for `FlintMath`. ## Tests 33 coprocessor tests pass. New `flint_math_unavailable_without_feature` confirms factory returns `None` without `--features flint`. The 8 flint-specific tests (poly GCD, mul, rem, content, nth-root, binomial) run only when `--features flint` is active and FLINT is installed. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 9af87ba commit cbd9449

19 files changed

Lines changed: 3055 additions & 6 deletions

File tree

.machine_readable/6a2/STATE.a2ml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,9 +42,10 @@ target-claim-id = "echidna-phase1a-tptp-atps / echidna-phase1b-frontier-fol"
4242
[[expansion-roadmap.phase]]
4343
id = "phase-2"
4444
title = "Computer-algebra (FLINT FFI + subprocess CAS family)"
45-
status = "available-for-claim"
45+
status = "phase-2a-complete"
4646
adds-backends = ["FLINT", "PARI/GP", "Maxima", "Singular", "GAP", "Macaulay2"]
4747
target-claim-id = "echidna-phase2a-cas-libraries / echidna-phase2b-cas-subprocess"
48+
notes = "Phase 2a landed 2026-04-26: FLINT FFI coprocessor backend (CoprocessorKind::FlintMath, Tier 3 LibraryWrapped, --features flint). Adds FlintPolyGcd/Mul/Rem/Content + FlintNthRoot + FlintBinomial ops, Polynomial outcome variant. 8 unit tests; factory returns None gracefully without the feature. Phase 2b (subprocess CAS: PARI/GP, Maxima, Singular, GAP, Macaulay2) still available for claim."
4849

4950
[[expansion-roadmap.phase]]
5051
id = "phase-3"

Cargo.toml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -110,6 +110,7 @@ echidna-core = { path = "crates/echidna-core" }
110110
[features]
111111
default = []
112112
chapel = [] # Enable Chapel parallel proof search (requires Zig FFI library)
113+
flint = [] # Enable FLINT CAS coprocessor (requires system libflint, LGPL-3)
113114
spark = [] # Enable SPARK-verified axiom-policy (requires libechidna_spark from GPRbuild)
114115
verisim = [ # Enable VeriSimDB persistent proof storage (8-modality octads)
115116
"dep:ciborium",

build.rs

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,46 @@ fn main() {
5050
println!("cargo:rerun-if-changed=src/zig/ffi/axiom_spark_bridge.zig");
5151
}
5252

53+
// FLINT CAS coprocessor (in-process, the only CAS we link rather than exec)
54+
#[cfg(feature = "flint")]
55+
{
56+
// Try pkg-config first; fall back to a bare -lflint on the standard
57+
// library path. FLINT is LGPL-3 and compatible with the PMPL/MPL-2.0
58+
// fallback licence under which ECHIDNA is distributed.
59+
let found_via_pkg_config = std::process::Command::new("pkg-config")
60+
.args(["--exists", "flint"])
61+
.status()
62+
.map(|s| s.success())
63+
.unwrap_or(false);
64+
65+
if found_via_pkg_config {
66+
// Let pkg-config emit the full set of link flags.
67+
if let Ok(output) = std::process::Command::new("pkg-config")
68+
.args(["--libs", "flint"])
69+
.output()
70+
{
71+
let flags = String::from_utf8_lossy(&output.stdout);
72+
for flag in flags.split_whitespace() {
73+
if let Some(path) = flag.strip_prefix("-L") {
74+
println!("cargo:rustc-link-search=native={path}");
75+
} else if let Some(lib) = flag.strip_prefix("-l") {
76+
println!("cargo:rustc-link-lib=dylib={lib}");
77+
}
78+
}
79+
}
80+
} else {
81+
// No pkg-config entry; attempt bare link on the system library path.
82+
println!("cargo:rustc-link-lib=dylib=flint");
83+
println!(
84+
"cargo:warning=FLINT not found via pkg-config — \
85+
trying bare -lflint. Install FLINT (LGPL-3) and ensure \
86+
its headers are on the include path."
87+
);
88+
}
89+
90+
println!("cargo:rerun-if-changed=src/rust/coprocessor/flint.rs");
91+
}
92+
5393
// Chapel parallel proof search bridge
5494
#[cfg(feature = "chapel")]
5595
{

0 commit comments

Comments
 (0)