META.a2ml

# SPDX-License-Identifier: MPL-2.0
# META.a2ml — Project meta-information
# Converted from META.scm on 2026-03-15

[metadata]
project = "echidna"
full-name = "Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance"
author = "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"
license = "MPL-2.0"
standard = "RSR 2026"
version = "2.3.0"
last-updated = "2026-10-05"
status = "active"

[project-context]
name = "echidna"
completion-percentage = 100  # mirrors STATE.a2ml (the authority for status); v2.3.0 release scope only
phase = "v2.3.0 released — see STATE.a2ml for the current phase"
notes = """
2026-04-28: corpus subsystem expanded into an N-dimensional / 8-
modality / cross-prover index, with simulated-annealing design-search
and 007 swarm dispatcher driving it. See docs/CORPUS.adoc and
docs/decisions/2026-04-28-corpus-and-design-search.adoc.
"""

[dependencies]
primary = ["Rust", "Julia", "AffineScript", "Idris2", "Zig"]
secondary = ["Chapel", "Bun", "Guix"]

[interfaces]
graphql = 8081
grpc = 50051
rest = 8000

# ─────────────────────────────────────────────────────────────────────────────
# Saturation campaign 2026-06-01 — additive surface declaration
# Branch: prover-corpus-saturation. ADR: docs/decisions/2026-06-01-saturation-campaign.adoc
# ─────────────────────────────────────────────────────────────────────────────

[saturation-campaign]
design-principle = "Saturation campaign 2026-06-01 — push corpus/vocab/arbitration to marginal-benefit limit while preserving heuristic-adapter quality contract"

[saturation-campaign.new-modules]
corpus = [
  "src/rust/corpus/isabelle.rs",
  "src/rust/corpus/metamath.rs",
  "src/rust/corpus/mizar.rs",
  "src/rust/corpus/hol_light.rs",
  "src/rust/corpus/hol4.rs",
  "src/rust/corpus/dafny.rs",
  "src/rust/corpus/why3.rs",
  "src/rust/corpus/fstar.rs",
  "src/rust/corpus/acl2_books.rs",
  "src/rust/corpus/tptp.rs",
  "src/rust/corpus/smtlib.rs",
  "src/rust/corpus/proofnet.rs",
  "src/rust/corpus/minif2f.rs",
  "src/rust/corpus/spark_ada.rs",
  "src/rust/corpus/creusot.rs",
  "src/rust/corpus/profile.rs",
]
verification = [
  "src/rust/verification/bayesian_arbiter.rs",
  "src/rust/verification/dempster_shafer.rs",
  "src/rust/verification/pareto_arbiter.rs",
]
exchange = [
  "src/rust/exchange/tptp.rs",
  "src/rust/exchange/smtlib.rs",
  "src/rust/exchange/smtcoq.rs",
  "src/rust/exchange/lambdapi.rs",
]

[saturation-campaign.new-data]
synonyms = [
  "data/synonyms/isabelle_afp.toml",
  "data/synonyms/metamath.toml",
  "data/synonyms/mizar.toml",
  "data/synonyms/hol_light.toml",
  "data/synonyms/hol4.toml",
  "data/synonyms/dafny.toml",
  "data/synonyms/why3.toml",
  "data/synonyms/fstar.toml",
  "data/synonyms/acl2.toml",
  "data/synonyms/_msc2020.toml",
  "data/synonyms/_wordnet_math.toml",
  "data/synonyms/_conceptnet_seed.toml",
  "data/synonyms/_verification_systems.toml",
]

[saturation-campaign.new-docs]
docs = [
  "docs/architecture/VERISIM-ER-SCHEMA.adoc",
  "docs/CORPUS-ADAPTERS.adoc",
  "docs/decisions/2026-06-01-saturation-campaign.adoc",
  "docs/handover/PROVER-CORPUS-SATURATION-LANE.adoc",
]

[saturation-campaign.new-schemas]
schemas = [
  "crates/echidna-wire/schemas/verisim_er.capnp",
]

[saturation-campaign.testing]
new-tests-passing = 139
heuristic-limit-ignored = 1
heuristic-limit-ignored-list = [
  "corpus::dafny::tests::detects_datatype_and_extern",
]

[self-proof-ci]
reviewed-on = "2026-09-25"
fast-corpus-workflow = ".github/workflows/dogfood-proofs-ci.yml"
abi-workflow = ".github/workflows/idris2-abi-ci.yml"
safety-workflow = ".github/workflows/proof-safety.yml"
weekly-workflow = ".github/workflows/verification-proofs-cron.yml"
weekly-scope = "Isabelle base HOL only; algebra and Mizar repairs remain in #280"
local-recipes = "Justfile: proofs-coq, proofs-lean, proofs-agda, proofs-idris, proofs-isabelle"
closure-evidence = "docs/reports/2026-09-25-issue-maintenance.adoc"