diff --git a/.machine_readable/descriptiles/STATE.a2ml b/.machine_readable/descriptiles/STATE.a2ml index ec6586c..6afef11 100644 --- a/.machine_readable/descriptiles/STATE.a2ml +++ b/.machine_readable/descriptiles/STATE.a2ml @@ -5,9 +5,9 @@ [metadata] project = "echidnabot" version = "0.1.0" -last-updated = "2026-06-02" +last-updated = "2026-10-09" status = "active" -session = "Production-hardening wave 2026-06-02: JSON logging (#63) + graceful shutdown (#64) + OpenTelemetry tracing (#65) + Docker Compose stack (#69) + Codeberg adapter scaffold (#74) + canonical-source two-purpose split (#55) + contractile family completion (#77 + #78); rsa phantom dep / sqlx default-features trim (#46); SHA-pin bumps (#50); workflow routing through standards reusables (#54); governance SHA pin (#53); echo-types audit (#48); panic-attack classifications (#47); doc maxout (#49); CITATION harmonised (#72). Test count 142+ (137 baseline + 6 new obs + scatter)." +session = "Issue #173: re-point shared trust kernel to echidna-core 0.2.0 on upstream main; local slug and contract parser retained. Build and test blocked: Cargo is not installed in this sandbox; draft PR pending verification." [project-context] name = "Echidnabot" @@ -441,3 +441,16 @@ file-4 = "Two commits (7052195 + 1b465ba) on main branch with detailed commit me [history.retired-root-state] last-updated = "2026-04-26" # seam test: 7a mode-routing + 7b corpus-bridge end-to-end session = "seam test DONE (tests/seam_test.rs, 15 tests); smoke.rs mode_selector bug fixed; lifecycle.rs unused-import cleaned; historical suite counts recorded as 137 lib + 17 lifecycle + 32 integration + 12 property + 15 seam + 8 smoke (sum 221; the retired 184 aggregate was inconsistent and is not a current test result)" + +[session-2026-10-09-trust-kernel] +issue = "#173" +upstream-rev = "645d7a2489c644706210e171acba6f52741ad3b8" +upstream-provenance = "GitHub commits/main API returned this full rev on 2026-10-09; echidna-core 0.2.0 re-exports echidna-core-creusot as trust." +changes = [ + "Re-point Cargo.toml and both trust-module import/doc paths to echidna-core::trust; no algorithm changes.", + "Remove stale rename follow-ups; preserve main-only pin policy, local ProverKind slug and local prove_result parser.", + "Update Cargo.lock using pinned upstream manifests and strum 0.28.0 / strum_macros 0.28.0 records from its Cargo.lock; Cargo regeneration remains unverified.", +] +validation = "cargo build and cargo test both attempted, exit 127: cargo: command not found. Trust unit tests not run." +coordination = "#166 remains open, but this checkout already pins tracing-opentelemetry 0.34 and rustls 0.23.45. No OTel or TLS dependency changes made; no security or CI pass claimed." +follow-up = "Run cargo build and cargo test with repository-pinned Rust 1.99.0, confirm lockfile resolution and trust unit tests before marking draft PR ready." diff --git a/Cargo.lock b/Cargo.lock index 1f76085..17e128b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -198,7 +198,7 @@ dependencies = [ "proc-macro-crate", "proc-macro2", "quote", - "strum", + "strum 0.27.2", "syn 2.0.117", "thiserror", ] @@ -1109,9 +1109,22 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "92773504d58c093f6de2459af4af33faa518c13451eb8f2b5698ed3d36e7c813" [[package]] -name = "echidna-core-spark" +name = "echidna-core" +version = "0.2.0" +source = "git+https://github.com/hyperpolymath/echidna?rev=645d7a2489c644706210e171acba6f52741ad3b8#645d7a2489c644706210e171acba6f52741ad3b8" +dependencies = [ + "anyhow", + "echidna-core-creusot", + "serde", + "serde_json", + "serde_json_canonicalizer", + "strum 0.28.0", +] + +[[package]] +name = "echidna-core-creusot" version = "0.1.0" -source = "git+https://github.com/hyperpolymath/echidna?rev=b761b3a832981be51d4e88076ef1b90fe5037e9c#b761b3a832981be51d4e88076ef1b90fe5037e9c" +source = "git+https://github.com/hyperpolymath/echidna?rev=645d7a2489c644706210e171acba6f52741ad3b8#645d7a2489c644706210e171acba6f52741ad3b8" dependencies = [ "serde", ] @@ -1130,7 +1143,7 @@ dependencies = [ "clap", "config", "criterion", - "echidna-core-spark", + "echidna-core", "gitbot-shared-context", "hex", "hmac 0.13.0", @@ -4072,7 +4085,16 @@ version = "0.27.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "af23d6f6c1a224baef9d3f61e287d2761385a5b88fdab4eb4c6f11aeb54c4bcf" dependencies = [ - "strum_macros", + "strum_macros 0.27.2", +] + +[[package]] +name = "strum" +version = "0.28.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9628de9b8791db39ceda2b119bbe13134770b56c138ec1d3af810d045c04f9bd" +dependencies = [ + "strum_macros 0.28.0", ] [[package]] @@ -4087,6 +4109,18 @@ dependencies = [ "syn 2.0.117", ] +[[package]] +name = "strum_macros" +version = "0.28.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ab85eea0270ee17587ed4156089e10b9e6880ee688791d45a905f5b1ca36f664" +dependencies = [ + "heck", + "proc-macro2", + "quote", + "syn 2.0.117", +] + [[package]] name = "subtle" version = "2.6.1" diff --git a/Cargo.toml b/Cargo.toml index 4a9ac68..cf6a860 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -30,12 +30,9 @@ gitbot-shared-context = { version = "0.1.0", git = "https://github.com/hyperpoly # ECHIDNA trust kernel. Canonical trust-level algorithm and source-level # axiom scanner, shared with ECHIDNA so echidnabot no longer re-implements -# them. Pinned by full rev (immutable). At this rev the crate is still named -# `echidna-core-spark`; it is being renamed `echidna-core-creusot` upstream, -# and the trust types are meant to move into `echidna-core` proper. Follow-up: -# re-point this line once that lands on echidna `main` (see -# docs/ECHIDNA-INTEGRATION.adoc). -echidna-core-spark = { git = "https://github.com/hyperpolymath/echidna", rev = "b761b3a832981be51d4e88076ef1b90fe5037e9c" } +# them via echidna-core 0.2.0's stable `trust` surface. Pinned by full rev +# on echidna `main` (see docs/ECHIDNA-INTEGRATION.adoc). +echidna-core = { git = "https://github.com/hyperpolymath/echidna", rev = "645d7a2489c644706210e171acba6f52741ad3b8" } # Minimum-version handshake with the ECHIDNA server. semver = "1" diff --git a/docs/ECHIDNA-INTEGRATION.adoc b/docs/ECHIDNA-INTEGRATION.adoc index cea8ecd..deca593 100644 --- a/docs/ECHIDNA-INTEGRATION.adoc +++ b/docs/ECHIDNA-INTEGRATION.adoc @@ -13,30 +13,28 @@ _proved_ mean different things and none implies the next. `src/trust/confidence.rs` and `src/trust/axiom_tracker.rs` no longer carry their own algorithms. -* The trust *level* comes from `echidna_core_spark::compute_trust_level` +* The trust *level* comes from `echidna_core::trust::compute_trust_level` (ECHIDNA's trust kernel). echidnabot only maps its inputs onto ECHIDNA's `TrustFactors`. `certificate_verified` is always `false`, because echidnabot never checks a certificate itself. * The proof-*source* axiom scan is ECHIDNA's - `echidna_core_spark::axiom_tracker::AxiomTracker`, called through + `echidna_core::trust::axiom_tracker::AxiomTracker`, called through `AxiomTracker::scan_source`. * The prover-*output* text scan (`AxiomTracker::scan`, for example Lean's "declaration uses 'sorry'") stays local. ECHIDNA has no equivalent. -The dependency is a git dependency pinned by full rev -(`b761b3a832981be51d4e88076ef1b90fe5037e9c`, on echidna `main`). A path -dependency would break standalone builds. - -Status: implemented and tested (unit tests in both modules). The kernel's -Creusot annotations are ECHIDNA's. echidnabot does not claim they are -proved. - -=== Follow-up: crate rename - -At the pinned rev the crate is named `echidna-core-spark`. It is not SPARK. -Upstream intends to rename it (`echidna-core-creusot`) and to move the trust -types into `echidna-core`. When either change lands on echidna `main`, update -the `Cargo.toml` line and the `use` paths. Do not pin to an unmerged branch. +The dependency is `echidna-core` 0.2.0, whose stable `trust` surface +re-exports the `echidna-core-creusot` kernel unchanged (including `pareto`). +It is a git dependency pinned by full rev +(`645d7a2489c644706210e171acba6f52741ad3b8`, verified on echidna `main` +on 2026-10-09). Do not pin to an unmerged branch. A path dependency would +break standalone builds. + +Status: implemented, with existing unit tests in both modules. Verification +of the 2026-10-09 dependency re-point is pending: `cargo build` and +`cargo test` could not run in the editing sandbox (Cargo is not installed). +The kernel's Creusot annotations are ECHIDNA's. echidnabot does not claim +they are proved. == Prover identifiers diff --git a/src/trust/axiom_tracker.rs b/src/trust/axiom_tracker.rs index 92de012..6a06ff9 100644 --- a/src/trust/axiom_tracker.rs +++ b/src/trust/axiom_tracker.rs @@ -19,14 +19,14 @@ //! Two scanners live here and they read different things: //! //! - [`AxiomTracker::scan_source`] reads the **proof source** and delegates to -//! ECHIDNA's canonical scanner (`echidna_core_spark::axiom_tracker`), which +//! ECHIDNA's canonical scanner (`echidna_core::trust::axiom_tracker`), which //! skips comment lines and ECHIDNA's own scaffold markers. This is the //! primary signal and is shared with ECHIDNA, not re-implemented. //! - [`AxiomTracker::scan`] reads the **prover's output text** (for example //! Lean's "declaration uses 'sorry'"). ECHIDNA has no equivalent, so this //! stays local, as a fallback for when the source is unavailable. -use echidna_core_spark::axiom_tracker::{ +use echidna_core::trust::axiom_tracker::{ AxiomTracker as EchidnaAxiomTracker, AxiomUsage, DangerLevel, }; use serde::{Deserialize, Serialize}; diff --git a/src/trust/confidence.rs b/src/trust/confidence.rs index 5b350f0..f5c3d09 100644 --- a/src/trust/confidence.rs +++ b/src/trust/confidence.rs @@ -4,7 +4,7 @@ //! Proof confidence level assessment //! //! The trust-level *algorithm* is ECHIDNA's, not echidnabot's: every call -//! goes through [`echidna_core_spark::compute_trust_level`] (the Creusot- +//! goes through [`echidna_core::trust::compute_trust_level`] (the Creusot- //! annotated kernel shared with ECHIDNA). This module only translates //! echidnabot's inputs (prover slug, status, artefacts, axiom scan) into //! ECHIDNA's [`TrustFactors`] and wraps the answer in a report. @@ -15,8 +15,8 @@ //! `echidna.prove.result/1` object, that is the *receipt* and is preferred; //! see [`crate::dispatcher::TrustSource`]. -use echidna_core_spark::axiom_tracker::DangerLevel; -use echidna_core_spark::{compute_trust_level, ProverClass, TrustFactors, TrustLevel}; +use echidna_core::trust::axiom_tracker::DangerLevel; +use echidna_core::trust::{compute_trust_level, ProverClass, TrustFactors, TrustLevel}; use serde::{Deserialize, Serialize}; use crate::dispatcher::{ProofStatus, ProverKind};