From 8d086ab51222adb3134c6ede82ee363fe2e8e248 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Fri, 9 Oct 2026 18:13:18 +0000 Subject: [PATCH 1/2] feat(metadata): land echidna_chora.deed deed-era baseline (standards#837) First repo deed under the estate one-deed-per-repo doctrine, following the proof-burrower_chora.deed precedent. Translated per the standards 1-formats/deed/mappings/ frame: - family 1 (CLADE.a2ml): identity, clade, forges, lineage, status; clade names verbatim from gv-clade-index verisim/seed/clades.a2ml; :repo-uuid carries the RFC 4122 name input, never the retired hex - family 2 (ECOSYSTEM.a2ml): the ecosystem clause incl. all nine related-project edges, verbatim Fail-closed, per the mapping frame: no (meta ...) clause (this repo's META.a2ml predates the family-2 field table and needs a table-extension review), and ECOSYSTEM's deployment/corpus/vocab/exchange/self-proof sections stay in the a2ml surface. STATE (family 3) and 0-AI-MANIFEST (family 7) translations remain owner-pending in standards. Deviations from the sources (standalone lineage parent, status history note) are recorded in the deed header. The .a2ml descriptiles stay until their consumers move to the deed; identity/status edits touch both surfaces until then. Passes deed_lint.py (deed.abnf) and .github/hooks/validate-a2ml.sh. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- echidna_chora.deed | 82 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 82 insertions(+) create mode 100644 echidna_chora.deed diff --git a/echidna_chora.deed b/echidna_chora.deed new file mode 100644 index 00000000..34136636 --- /dev/null +++ b/echidna_chora.deed @@ -0,0 +1,82 @@ +;; SPDX-License-Identifier: MPL-2.0 +;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +; +; The repo deed of echidna (one-deed-per-repo doctrine, standards#837). +; Scope of this first deed (2026-10-09): identity, clade, forges, lineage +; and status translated from .machine_readable/CLADE.a2ml (family 1), plus +; the ecosystem clause translated from .machine_readable/descriptiles/ +; ECOSYSTEM.a2ml (family 2), per standards 1-formats/deed/mappings/ +; clade-to-repo-deed.adoc and meta-ecosystem-to-repo-deed.adoc. Clade +; names follow gv-clade-index verisim/seed/clades.a2ml verbatim. +; +; Not translated (fail-closed, per the mapping frame): +; - the (meta ...) clause: echidna's META.a2ml predates the family-2 +; field-table shape and needs a table-extension review first +; - ECOSYSTEM.a2ml [deployment], [corpus-sources], [vocab-sources], +; [proof-exchange-standards] and [self-proof-ci]: not in the family-2 +; table, so they stay in ECOSYSTEM.a2ml +; - STATE.a2ml (family 3) and 0-AI-MANIFEST.a2ml (family 7): owner +; decisions pending in standards (state-v1-decision.adoc, +; ai-manifest-decision.adoc); nothing here pre-empts them +; The .a2ml surfaces above are still read by consumers (session protocol, +; openssf-compliance, contractiles Justfile), so they stay until their +; consumers move to this deed; until then a change to identity or status +; must be made in both places. +; +; Deviations recorded: CLADE.a2ml [lineage] parent carried a description +; ("Neurosymbolic theorem proving - neural proof synthesis") although the +; lineage type is standalone; the deed carries "" per the parent-is-the- +; monorepo-parent-never-a-description doctrine. The status history note +; was the clade-status-backfill placeholder; it is re-derived here. +(repo-deed + :schema-version "1.0.0" + :canonical-name "echidna" + :beholding-chora #u5"estate/chora" + :repo-uuid #u5"github.com/hyperpolymath/echidna" + + (identity :primary-forge github + :owner "hyperpolymath" + :prefixed-name "fv-echidna") + + (clade :primary fv + :primary-name "Formal Verification & Proofs" + :secondary (ax) + :assigned "2026-03-16" + :rationale "") + + (forges :github "hyperpolymath/echidna" + :gitlab "hyperpolymath/echidna" + :bitbucket "hyperpolymath/echidna") + + (lineage :type standalone + :parent "" + :born "2026-03-16" + :previous-names ()) + + (status :phase active + :since "2026-03-16" + :present #t + :aliases () + :merged-into "" + :superseded-by "" + :successors () + :ended "" + (history + (entry :phase active + :since "2026-03-16" + :note "trust-hardened neurosymbolic theorem prover; proving core of the hyperpolymath estate"))) + + (ecosystem :project "echidna" + :ecosystem "hyperpolymath" + :position-type "component" + :purpose "Trust-hardened neurosymbolic theorem proving platform. 141 ProverKind variants across 105 backend implementations, 12 exposed by default at GET /api/provers (Agda, Coq, Lean 4, Isabelle/HOL, Z3, CVC5, Metamath, HOL Light, Mizar, PVS, ACL2, HOL4); canonical tier table and count semantics in docs/PROVER_COUNT.adoc. Sandboxed solver execution (Podman/bubblewrap), proof certificate checking, axiom tracking, GNN-guided proof search, Julia ML inference layer." + :coordination "" + (related :name "proven-servers (nesy-solver-api)" :relationship consumer :notes "nesy-solver-api calls /api/verify on echidna-nesy.flycast:8090. Cold-start grace 90s.") + (related :name "hypatia" :relationship sibling-neurosym :notes "Hypatia performs neurosymbolic CI scanning; echidna does theorem proving. Both are Tier 2 formal verification tools.") + (related :name "verisimdb" :relationship active-integration :notes "Corpus emits 8-modality octads (corpus/octad.rs) compatible with /api/v1/octads. Round-trip verified; HTTP push deferred.") + (related :name "neural-foundations" :relationship monorepo-satellite :notes "echidna is mirrored as a submodule/satellite inside neural-foundations.") + (related :name "maa-framework" :relationship sibling :notes "Absolute-zero and related MA/ML tools in same neurosymbolic tier.") + (related :name "echo-types" :relationship active-consumer :notes "Echidna's design-search drove the Phase 1.3 _≤_ redesign + unbudgeted wf-<ᵇʳᶠ rank-function recommendations. Handoff document at echo-types/docs/echidna-design-search-2026-04-28.adoc. 640 entries indexed.") + (related :name "januskey/reversible-core" :relationship planned-integration :notes "Bennettian reversibility substrate for the SA annealer trace ledger. Not yet wired.") + (related :name "jtv (Lean 4)" :relationship indexed :notes "147 entries verified during Lean adapter rollout.") + (related :name "eclexia (Idris 2 ABI)" :relationship indexed :notes "93 entries verified during Idris 2 adapter rollout."))) From 110b72ae582a478bb065b30c2ddfb8948154e1ee Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Fri, 9 Oct 2026 18:13:54 +0000 Subject: [PATCH 2/2] fix(metadata): refresh STATE past the integrations wave; fix manifest drift STATE.a2ml was last touched 2026-06-13; the 2026-10-05 integrations wave (prove --output json, echidna-core 0.2.0, creusot rename, Zig FFI CI) and today's deed baseline are now journaled per the session protocol, and last-updated advances. 0-AI-MANIFEST.a2ml drift fixed: - full-version tracked a stale 1.x release; now follows Cargo.toml - tech-stack secondary line read AffineScript+Deno with a stale file count; Deno was banned estate-wide 2026-09-22 (JS-RUNTIME-POLICY) and the UI runs on Bun per CLAUDE.md - canonical-locations gains the deed pointer CHANGELOG [Unreleased] records the deed baseline and these fixes. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .machine_readable/descriptiles/STATE.a2ml | 13 ++++++++++++- 0-AI-MANIFEST.a2ml | 5 +++-- CHANGELOG.adoc | 22 ++++++++++++++++++++++ 3 files changed, 37 insertions(+), 3 deletions(-) diff --git a/.machine_readable/descriptiles/STATE.a2ml b/.machine_readable/descriptiles/STATE.a2ml index 1e0a1b1e..5bba2212 100644 --- a/.machine_readable/descriptiles/STATE.a2ml +++ b/.machine_readable/descriptiles/STATE.a2ml @@ -9,7 +9,7 @@ type = "state-file" [metadata] project = "echidna" version = "2.3.0" -last-updated = "2026-06-13" +last-updated = "2026-10-09" status = "active" release-tag = "v2.3.0" @@ -18,6 +18,17 @@ name = "echidna" completion-percentage = 100 phase = "v2.3.0 Released — saturation+typing (#198) + GNN training wiring (#207) + dispatcher all-17-adapters (PR pending SPDX hook) + comprehensive contractile family (#214) + first owner-authorised GNN training run completed (best MRR 0.92)" +[session-2026-10-09-deed-baseline] +summary = "Deed-era baseline landed; STATE refreshed past the 2026-10-05 integrations wave" +changes = [ + "Recorded the integrations wave that postdated the last STATE touch (2026-06-13): echidna prove --output json emitting echidna.prove.result/1 (JCS-canonical I-JSON), echidna-core 0.2.0 consumable by echidnabot + proof-burrower, echidna-core-spark renamed echidna-core-creusot with the trust kernel re-exported as echidna_core::trust, ffi/zig building and CI-gated (zig-ffi-ci.yml) — all in CHANGELOG.adoc [Unreleased]", + "New echidna_chora.deed at repo root: first deed under the one-deed-per-repo doctrine (standards#837), translated from CLADE.a2ml (family 1) and ECOSYSTEM.a2ml (family 2) per standards 1-formats/deed/mappings/; clade names verbatim from gv-clade-index verisim/seed/clades.a2ml; passes deed_lint (deed.abnf)", + "Fail-closed, per the mapping frame: no (meta …) clause yet — this repo's META.a2ml predates the family-2 field table; STATE (family 3) and 0-AI-MANIFEST (family 7) translations stay owner-pending in standards", + "The ten stale AGPL-3.0-or-later SPDX headers under HOL-o-extension/, audits/ and training_data/ were left in place by design: D262's recorded plan (CHANGELOG [Unreleased], docs/DEBT.adoc P0) rewrites them inside the a2ml->deed conversion, so this baseline does not touch an owner-gated licensing surface early", + "0-AI-MANIFEST.a2ml drift fixed: full-version 1.6.0 -> 2.3.0, UI runtime Deno -> Bun (Deno banned estate-wide 2026-09-22), deed added to canonical-locations", +] +consumers-note = ".machine_readable descriptiles stay until their consumers move to the deed; until then identity/status changes go in both places" + [session-2026-06-13-dogfood-proof-ci] summary = "Proof corpus repaired and gated in CI (PR #234, squash-merged to main 2026-06-06)" pr = "https://github.com/hyperpolymath/echidna/pull/234" diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index 9fac6abd..e280868c 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -10,7 +10,7 @@ version = "1.1" project = "echidna" type = "neurosymbolic-theorem-prover" -full-version = "1.6.0" +full-version = "2.3.0" license = "MPL-2.0" author = "Jonathan D.A. Jewell " repo = "https://github.com/hyperpolymath/echidna" @@ -31,6 +31,7 @@ repo = "https://github.com/hyperpolymath/echidna" # node_modules/ — dependencies [canonical-locations] +deed = "echidna_chora.deed" state-files = ".machine_readable/" state = ".machine_readable/descriptiles/STATE.a2ml" meta = ".machine_readable/descriptiles/META.a2ml" @@ -47,7 +48,7 @@ container = "container/" [tech-stack] primary = "Rust (141 ProverKind variants over 105 backend implementations — see docs/PROVER_COUNT.adoc; trust pipeline, CLI, REPL, API servers)" -secondary = "Julia (ML inference, port 8090), AffineScript+Deno (UI, 33 files, zero TypeScript)" +secondary = "Julia (ML inference, port 8090), AffineScript+Bun (UI, TEA architecture, zero TypeScript; Deno banned estate-wide 2026-09-22)" optional = "Chapel (parallel proof dispatch)" abi = "Idris2 (7 modules, zero believe-me)" ffi = "Zig (4 shared libraries)" diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 0c1e751e..d17696c2 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -41,6 +41,28 @@ kernel tests never ran in CI. is a hard gate or that milestones 8c-M1..M3 are done; it records why Creusot does not run in CI. +==== Added — governance 2026-10-09 + +* *`+echidna_chora.deed+`* at the repo root: the first deed under the +estate one-deed-per-repo doctrine (standards#837), translated from +`+CLADE.a2ml+` (family 1) and `+ECOSYSTEM.a2ml+` (family 2) per the +standards `+1-formats/deed/mappings/+` frame, following the +`+proof-burrower_chora.deed+` precedent; clade names verbatim from the +gv-clade-index taxonomy seed; passes the normative `+deed.abnf+` +validator. The `+.a2ml+` descriptiles stay until their consumers move; +identity/status edits touch both surfaces until then (noted in the deed +header). + +==== Fixed — governance 2026-10-09 + +* `+0-AI-MANIFEST.a2ml+`: `+full-version+` was frozen at a stale 1.x +value; it now tracks `+Cargo.toml+`. The UI runtime line reads Bun +(Deno was banned estate-wide 2026-09-22; JS-RUNTIME-POLICY), and the +deed is listed under `+[canonical-locations]+`. +* `+.machine_readable/descriptiles/STATE.a2ml+`: refreshed past the +2026-10-05 integrations wave and recorded the deed baseline (session +protocol). + ==== Changed * *Licence: `+AGPL-3.0-or-later+` → `+MPL-2.0+` for code and the