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

.github/workflows/actions.lock

@@ -92,6 +92,10 @@ workflows:
         - 'actions/checkout@v7.0.1'
     '.github/workflows/workflow-linter.yml':
         - 'actions/checkout@v7.0.1'
+    '.github/workflows/zig-ffi-ci.yml':
+        - 'actions/checkout@v7.0.1'
+        - 'hyperpolymath/cicd-suite@main'
+        - 'mlugg/setup-zig@v2.2.1'
 dependencies:
     'actions/attest-build-provenance@v4.2.2':
         ref: 'v4.2.2'
@@ -172,6 +176,11 @@ dependencies:
         commit: 'sha1-0f8e8c99d88aeb3fbfd523f1ef2c6f762d10d64d'
         owner_id: 75048950
         repo_id: 623796603
+    'hyperpolymath/cicd-suite@main':
+        ref: 'main'
+        commit: 'sha1-d9ebcf99ad4593611b4fa0e18f09b03801f200e8'
+        owner_id: 6759885
+        repo_id: 1326697643
     'mlugg/setup-zig@v2.2.1':
         ref: 'v2.2.1'
         commit: 'sha1-d1434d08867e3ee9daa34448df10607b98908d29'

.github/workflows/chapel-ci.yml

@@ -123,7 +123,7 @@ jobs:
           version: 0.14.0
 
       - name: Build Zig FFI library (with Chapel stubs)
-        run: cd src/zig_ffi && zig build -Doptimize=ReleaseSafe
+        run: cd src/zig_ffi && zig build -Doptimize=ReleaseSafe -Dcpu=baseline  # baseline: the artifact runs on another runner (SIGILL otherwise)
 
       - name: Run Zig FFI tests (stub mode)
         run: cd src/zig_ffi && zig build test
@@ -219,7 +219,7 @@ jobs:
       - name: Build Zig FFI without stubs (links against real Chapel)
         run: |
           cd src/zig_ffi
-          zig build -Doptimize=ReleaseSafe -Dstubs=false
+          zig build -Doptimize=ReleaseSafe -Dcpu=baseline -Dstubs=false
 
       - name: Build Rust with real Chapel library
         run: |

.github/workflows/rust-ci.yml

@@ -104,16 +104,16 @@ jobs:
         # first push it happens, instead of silently re-resolving (which
         # masked the echidna#92 / echidna PR #128 dependabot major-bump
         # break for 24h). See standards#295.
-        run: cargo check --locked --all-targets
+        run: cargo check --locked --workspace --all-targets
 
       - name: Cargo fmt
         run: cargo fmt --all -- --check
 
       - name: Cargo clippy
-        run: cargo clippy --locked --all-targets -- -D warnings
+        run: cargo clippy --locked --workspace --all-targets -- -D warnings
 
   test:
-    timeout-minutes: 20
+    timeout-minutes: 30
     name: rust-ci / Cargo test
     runs-on: ubuntu-latest
     needs: [detect, check]
@@ -149,7 +149,9 @@ jobs:
 
       - name: Run tests
         # `--locked` — see Cargo check above.
-        run: cargo test --locked --all-targets
+        # `--workspace`: without it only the root package is tested, so the
+        # echidna-core (prove-result contract) and trust-kernel tests never ran.
+        run: cargo test --locked --workspace --all-targets
 
       - name: Write summary
         if: always()

.github/workflows/zig-ffi-ci.yml

@@ -0,0 +1,62 @@
+# This workflow is managed by gh actions-lock.
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# Zig FFI CI for echidna (ffi/zig): format, unit tests, and the estate
+# unified-api-adapter purity check (no std.fs / std.io in any .zig file).
+#
+# Before 2026-10-05 ffi/zig was built by no workflow and did not compile on
+# any Zig release (opaque Handle with fields, implicit libc). This job keeps
+# it compiling and tested. The library targets that link against the Rust
+# libechidna.so (integration tests, benchmarks) are not built here.
+#
+# Zig is pinned to 0.15.2, the version ffi/zig/build.zig is written for.
+name: Zig FFI CI
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  zig-ffi:
+    name: zig-ffi / fmt + test (ffi/zig)
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v7.0.1
+        with:
+          persist-credentials: false
+
+      - name: Install Zig
+        uses: mlugg/setup-zig@v2.2.1
+        with:
+          version: 0.15.2
+
+      - name: zig fmt --check
+        run: zig fmt --check ffi/zig/src ffi/zig/test ffi/zig/build.zig
+
+      - name: zig build test
+        working-directory: ffi/zig
+        run: zig build test --summary all
+
+  unified-api-adapter:
+    name: zig-ffi / unified-api-adapter purity
+    runs-on: ubuntu-latest
+    timeout-minutes: 5
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v7.0.1
+        with:
+          persist-credentials: false
+
+      - name: Zig unified-api-adapter check (hyperpolymath/cicd-suite)
+        uses: hyperpolymath/cicd-suite/actions/zig-unified-api-adapter-check@main

CHANGELOG.adoc

@@ -8,6 +8,39 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 === [Unreleased]
 
+==== Added — integrations 2026-10-05
+
+* *`+echidna prove --output json+`*: prints exactly one
+`+echidna.prove.result/1+` object (JCS-canonical I-JSON) on stdout, logs
+to stderr. Statuses `+verified+` / `+failed+` / `+error+` / `+timeout+` /
+`+unknown+`, mapped from `+ProverOutcome+`; `+trust.confidence+` is
+`+null+` unless receipt-backed. Human output stays the default. See
+`+docs/PROVE-RESULT-CONTRACT.adoc+`.
+* *`+echidna-core+` 0.2.0* is consumable by clients (echidnabot,
+proof-burrower): adds `+ProverKind+` (moved from `+echidna::provers+`,
+re-exported there, no source change for ECHIDNA), the
+`+echidna.prove.result/1+` type with a strict parser, and the trust
+kernel as `+echidna_core::trust+`. Git-dependency recipe and stability
+policy in `+crates/echidna-core/README.adoc+`.
+* *`+ffi/zig+` builds and is tested in CI* (`+zig-ffi-ci.yml+`, Zig
+0.15.2): it previously compiled on no Zig release. Pure Zig (page
+allocator, no libc); the estate unified-api-adapter purity check
+(`+hyperpolymath/cicd-suite+`) runs on every PR.
+
+==== Fixed — integrations 2026-10-05
+
+* ci(chapel): build the Zig FFI with `+-Dcpu=baseline+`; the artifact
+runs on a different runner, and native-CPU code crashed there with
+SIGILL in "Rust Build with Chapel Feature".
+* ci(rust): check, clippy and test now run with `+--workspace+`; before,
+only the root package was tested, so `+echidna-core+` and the trust
+kernel tests never ran in CI.
+* abi: `+EchidnaABI.Gnn+` and `+EchidnaABI.TacticRecord+` now declare
+`+%default total+` (both already type-check total).
+* docs(creusot): `+CREUSOT-SETUP.adoc+` no longer claims the Creusot job
+is a hard gate or that milestones 8c-M1..M3 are done; it records why
+Creusot does not run in CI.
+
 ==== Changed
 
 * *Licence: `+AGPL-3.0-or-later+` → `+MPL-2.0+` for code and the

crates/echidna-core-creusot/CREUSOT-SETUP.adoc

@@ -92,19 +92,40 @@ contract.
 All obligations in `+impl_invariants+` are designed to discharge quickly
 (< 30 s each on a modern workstation).
 
-=== 6 — CI integration
-
-`+.github/workflows/formal-verification.yml+` runs two jobs, both merge
-gates:
-
-* `+stable-tests+`: `+cargo test -p echidna-core-creusot+` on stable Rust
-(~10 s).
-* `+creusot-verify+`: `+cargo +nightly creusot+` with Why3 + Z3
-discharge. Requires `+apt-get install why3 z3 alt-ergo+` in the runner
-(Ubuntu 22.04+).
-
-Both were promoted to hard gates in Stage 8c-M3 (no
-`+continue-on-error+`).
+=== 6 — CI integration (what actually runs)
+
+`+.github/workflows/formal-verification.yml+` has two jobs:
+
+* `+stable-tests+`: `+cargo test -p echidna-core-creusot+` on stable Rust.
+It runs on pull requests that touch this crate, and the crate's tests
+also run in the workspace test job of `+rust-ci.yml+`. It checks the
+stable-Rust mirror of each stated obligation. It does not run Creusot.
+* `+creusot-verify+`: manual only (`+workflow_dispatch+`). It has never
+discharged an obligation.
+
+==== Why Creusot does not run in CI (measured 2026-10-05)
+
+. *The annotations do not compile under Creusot's macros.*
+`+cargo check -p echidna-core-creusot --features creusot+` fails with
+34 errors: `+creusot_contracts+` is unresolved (it is not a
+dependency), so `+ensures+`, `+requires+`, `+invariant+`, `+pure+` and
+`+snapshot!+` are unknown. No obligation has ever reached Why3.
+. *The toolchain pin is stale.* `+rust-toolchain.toml+` pins
+`+nightly-2024-05-01+`, which predates current Creusot releases.
+. *The install path in this guide is wrong for current Creusot.* Creusot
+is installed with its own `+INSTALL+` script, which provisions Why3 and
+`+why3find+` through opam; `+cargo install creusot+` does not do that.
+. *Adding `+creusot-contracts+` as an optional dependency would put a
+nightly-only crate in `+Cargo.lock+`*, which the stable `+--locked+`
+build and `+cargo audit+` also read.
+
+What it would take: pick one Creusot release, pin its nightly here and in
+the workflow, add `+creusot-contracts+` behind the `+creusot+` feature,
+rewrite the annotations against that release's logic syntax until
+`+cargo creusot+` type-checks them, install Creusot with its `+INSTALL+`
+script in the job, and only then make `+creusot-verify+` run on pull
+requests. Until a dispatch run discharges every obligation, call the
+annotations *stated, not proved*.
 
 === Annotation style
 
@@ -124,36 +145,23 @@ no-ops on stable Rust.
 |===
 |Milestone |Contents |Status
 |8c-M1 |`+rust-toolchain.toml+`, `+formal-verification.yml+`,
-`+just verify-trust-pipeline+` |*done*
+`+just verify-trust-pipeline+` |files exist; toolchain pin stale
 
 |8c-M2 |`+dominates+` marked `+#[pure]+`; `+compute+` ensures with
-`+^candidates+`; inner-loop `+#[invariant]+` for `+dominated+` |*done*
+`+^candidates+`; inner-loop `+#[invariant]+` for `+dominated+`
+|annotations written, never type-checked by Creusot
 
 |8c-M3 |Outer-loop invariant (`+snapshot!+` + prefix classification);
-Why3 CI hard gate |*done*
+Why3 CI hard gate |annotations written; *no CI gate* (see above)
 |===
 
-All three milestones are complete. The `+compute+` function now carries
-the full two-level invariant structure:
-
-* *Outer*: `+snapshot!(candidates)+` at entry + `+#[invariant]+`
-asserting
-[loweralpha]
-. objectives unchanged for all k, (b) `+is_pareto_optimal[k]+` correctly
-set for k < i.
-* *Inner*: `+dominated == (∃ k < j, k ≠ i : dominates(k, i))+`.
-
-The CI workflow (`+formal-verification.yml+`) is a hard gate: both
-`+stable-tests+` and `+creusot-verify+` must pass for a merge. If the
-nightly pin drifts, bump `+rust-toolchain.toml+` + the workflow’s
-`+toolchain:+` field together.
-
-This keeps the crate buildable on stable Rust at all times while still
-expressing every proof obligation in machine-verifiable syntax.
+An earlier version of this table marked all three milestones done and
+described both jobs as hard merge gates. That was not true: no obligation
+has been discharged (see "Why Creusot does not run in CI").
 
 === References
 
 * Creusot repository: https://github.com/creusot-rs/creusot
 * Why3 documentation: https://www.why3.org/
-* SPARK Adoption Plan: `+docs/design/SPARK_ADOPTION_PLAN.adoc+`
+* SPARK Adoption Plan: `+docs/design/SPARK_ADOPTION_PLAN.adoc+` (historical; this crate is Creusot, not SPARK)
 * Echidna ROADMAP Stage 8c: `+docs/ROADMAP.adoc+`

crates/echidna-core/Cargo.toml

@@ -2,13 +2,23 @@
 
 [package]
 name = "echidna-core"
-version = "0.1.0"
+version = "0.2.0"
 edition = "2021"
 authors = ["Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"]
 license = "MPL-2.0"
-description = "Canonical Term / Goal / ProofState / Tactic types for ECHIDNA, re-used by vcl-ut and any future proof-exchange client without depending on the full echidna binary."
+description = "Canonical ECHIDNA client types: Term / Goal / ProofState / Tactic, ProverKind, the echidna.prove.result/1 contract and the trust kernel, without depending on the full echidna binary."
 repository = "https://github.com/hyperpolymath/echidna"
 
 [dependencies]
 serde = { version = "1", features = ["derive"] }
 serde_json = "1"
+# ProverKind::from_str keeps its historical anyhow::Error error type.
+anyhow = "1"
+# ProverKind derives strum::EnumIter.
+strum = { version = "0.28.0", features = ["derive"] }
+# JCS (RFC 8785) canonical JSON for the echidna.prove.result/1 contract.
+serde_json_canonicalizer = "0.3"
+# Trust kernel (TrustLevel, compute_trust_level, axiom scanner), re-exported
+# as echidna_core::trust. Path dependency inside this repository; a git
+# dependency on echidna-core resolves it from the same commit.
+echidna-core-creusot = { path = "../echidna-core-creusot", version = "0.1.0" }

crates/echidna-core/README.adoc

@@ -0,0 +1,59 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+= echidna-core
+
+The types a client of ECHIDNA needs, without the full `echidna` crate:
+
+[cols="1,3",options="header"]
+|===
+| Module | Contents
+
+| `core`, `types` | `Term`, `Goal`, `ProofState`, `Tactic`, `TypeInfo`.
+| `prover_kind` | `ProverKind`, the backend enumeration, with `FromStr` and `Display`.
+| `prove_result` | `ProveResult`, the `echidna.prove.result/1` contract printed by `echidna prove --output json` (see `docs/PROVE-RESULT-CONTRACT.adoc`), with a JCS serialiser and a strict parser.
+| `trust` | The trust kernel re-exported from `echidna-core-creusot`: `TrustLevel`, `TrustFactors`, `ProverClass`, `compute_trust_level`, `combine_trust`, `axiom_tracker`, `pareto`.
+|===
+
+`echidna` re-exports these, so `echidna::ProverKind` and
+`echidna::provers::ProverKind` are the same type as
+`echidna_core::ProverKind`.
+
+== Using it from another repository
+
+The crate is not published to crates.io. Depend on it from git, pinned to a
+full commit SHA so the build is reproducible:
+
+[source,toml]
+----
+[dependencies]
+echidna-core = { git = "https://github.com/hyperpolymath/echidna", rev = "<full 40-character commit SHA on main>" }
+----
+
+Cargo finds the crate inside the repository by name. Its path dependency on
+`echidna-core-creusot` resolves from the same commit, so nothing else is
+needed. Do not use a `path = "../echidna/..."` dependency in a published
+repository: it only builds on a machine with that checkout.
+
+Dependencies it brings: `serde`, `serde_json`, `anyhow`, `strum`,
+`serde_json_canonicalizer`, and `echidna-core-creusot` (which needs only
+`serde`).
+
+== Stability
+
+The crate follows Semantic Versioning, read the Cargo way for 0.x: a change
+in the minor number (0.2 to 0.3) may break, a change in the patch number
+does not.
+
+* Stable from 0.2.0: the module paths above, the `ProverKind` variant
+  names (they are its serde form), the `ProveResult` fields and the
+  `echidna.prove.result/1` wire format, and the `trust` items listed above.
+* Adding a `ProverKind` variant is not breaking for ECHIDNA's purposes; keep
+  a wildcard arm when you match on it.
+* The trust kernel's Creusot annotations are stated, not proved (see
+  `crates/echidna-core-creusot/CREUSOT-SETUP.adoc`). Its behaviour is
+  covered by stable-Rust tests.
+
+== History
+
+* 0.2.0 (2026-10-05): added `prover_kind`, `prove_result` and `trust`.
+  `ProverKind` moved here from `echidna::provers`; nothing was removed.
+* 0.1.0: `core` and `types`.