feat: echidna prove --output json, echidna-core client crate, Zig FFI CI

[hyperpolymath]

Follow-up to #407 (merged as b97a799), so this PR is based on main, not stacked.

What this does

1. echidna prove --output json implements the shared echidna.prove.result/1 contract.

• stdout carries exactly one JCS-canonical (RFC 8785) I-JSON object; logs go to stderr.
• status comes from ProverOutcome::prove_status: Proved → verified, NoProofFound → failed, Timeout → timeout, InconsistentPremises → unknown, and input, prover or system failures → error. Failures before the check (no backend, unreadable file, parse error) are also error objects.
• Exit code is 0 iff verified.
• trust.confidence is null unless a receipt backs it. This is the epistemic-types receipt/warrant pattern, used as a pattern only, not as a dependency. This path checks no certificate, so the value is always null. trust.axioms comes from ECHIDNA's axiom tracker.
• Human output is still the default and unchanged.
• Docs: docs/PROVE-RESULT-CONTRACT.adoc.

2. echidna-core 0.2.0 can now be used by clients such as echidnabot and proof-burrower.

• ProverKind moved into the crate. echidna::ProverKind and echidna::provers::ProverKind re-export it, so no ECHIDNA source changed.
• Adds prove_result (the contract type, a JCS serialiser and a strict parser).
• Adds trust, a re-export of the echidna-core-creusot trust kernel that echidnabot already pins.
• The git-dependency recipe and the stability policy are in crates/echidna-core/README.adoc.

3. Zig FFI and the unified-api-adapter check.

• ffi/zig did not compile on any Zig release (0.14.1, 0.15.2 and 0.16.0 all failed) and no workflow built it.
• It now compiles in pure Zig (opaque Handle, page allocator, no libc).
• The new zig-ffi-ci.yml runs zig fmt --check, zig build test (45 tests) and the hyperpolymath/cicd-suite purity check.
• The only std.io use, in tentacles.zig, is gone, and poll_events gained tests.
• Scope: "check passing" means the purity grep passes. No Zig adapter library exists to adopt.

4. CI fixes.

• chapel-ci.yml builds Zig with -Dcpu=baseline. The artifact runs on a different runner, and that caused the SIGILL in "Rust Build with Chapel Feature" on main.
• rust-ci.yml check, clippy and test now pass --workspace. Before, only the root package was tested, so the echidna-core and trust-kernel tests never ran.

5. Idris2 ABI.

• Added %default total to EchidnaABI.Gnn and EchidnaABI.TacticRecord; the package still type-checks.
• Planted-positive control: a non-terminating function is rejected.
• CapnSchemas.idr and NeSyAssistTesting.idr are not in the ipkg, so CI does not check them. This is recorded in the wiki table.

6. Creusot: precisely why it is not in CI.

• cargo check -p echidna-core-creusot --features creusot fails with 34 errors, because creusot-contracts is not a dependency.
• The nightly pin is stale, and the documented install path is wrong for current Creusot.
• CREUSOT-SETUP.adoc no longer claims the job is a hard gate or that milestones 8c-M1..M3 are done. The annotations remain stated, not proved.

Verification (local, rustc 1.99.0)

• cargo fmt --all -- --check passes.
• cargo clippy --locked --workspace --all-targets -- -D warnings passes.
• cargo test --locked --workspace --all-targets passes.
• zig build test passes: 45/45 on Zig 0.15.2.
• idris2 --build src/abi/echidnaabi.ipkg passes on Idris2 0.7.0.
• gh actions-lock --no-fix is clean over 35 workflows.

Not in this PR

• absolute-zero as a cross-prover test corpus (ADOPT-NOW in the types fit map). It needs prover binaries in the live matrix and a pinned corpus manifest, which is out of this increment.
• UUID minting is unchanged. It is already centralised in src/rust/ids.rs, and this PR mints no IDs.

Deferred red checks (§5c)

• Rust Build — Real Chapel Library (allow-fail, L2.3+ gate): was already red on main before this PR. Deferred to ci: 'Rust Build — Real Chapel Library' fails to link (undefined chapel_* symbols) #408, which has acceptance criteria.

🤖 Generated with Claude Code

[coderabbitai]

Navigate logical layers of code changes, visualize relationships, and explore their blast radius.

Note

Currently processing new changes in this PR. This may take a few minutes, please wait...

⚙️ Run configuration

• Configuration used: Organization UI
• Review profile: ASSERTIVE
• Plan: Advanced
• Run ID: 9221bc52-8244-48b3-bce1-0997cb537e0a

📥 Commits

Reviewing files that changed from the base of the PR and between b97a799 and 018a5bf.

⛔ Files ignored due to path filters (2)

• .github/workflows/actions.lock is excluded by !**/*.lock
• Cargo.lock is excluded by !**/*.lock

📒 Files selected for processing (31)

• .github/workflows/chapel-ci.yml
• .github/workflows/rust-ci.yml
• .github/workflows/zig-ffi-ci.yml
• CHANGELOG.adoc
• crates/echidna-core-creusot/CREUSOT-SETUP.adoc
• crates/echidna-core/Cargo.toml
• crates/echidna-core/README.adoc
• crates/echidna-core/src/lib.rs
• crates/echidna-core/src/prove_result.rs
• crates/echidna-core/src/prover_kind.rs
• docs/PROVE-RESULT-CONTRACT.adoc
• docs/wikis/Home.md
• ffi/zig/src/boj.zig
• ffi/zig/src/capnp_bridge.zig
• ffi/zig/src/main.zig
• ffi/zig/src/provers/atp.zig
• ffi/zig/src/provers/declarative.zig
• ffi/zig/src/provers/vcl_ut.zig
• ffi/zig/src/tentacles.zig
• ffi/zig/src/typell.zig
• ffi/zig/test/benchmark.zig
• ffi/zig/test/core_native_test.zig
• ffi/zig/test/integration_test.zig
• src/abi/EchidnaABI/Gnn.idr
• src/abi/EchidnaABI/TacticRecord.idr
• src/rust/lib.rs
• src/rust/main.rs
• src/rust/prove_contract.rs
• src/rust/provers/mod.rs
• src/rust/provers/outcome.rs
• tests/prove_output_json.rs

 ___________________________________________________________
< Ultimately, we're all just debugging someone else's code. >
 -----------------------------------------------------------
  \
   \   \
        \ /\
        ( )
      .( o ).

✨ Finishing Touches

📝 Generate docstrings

• Commit to this branch
• Create a new PR

• Autopilot · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}