Merge branch 'main' into dependabot/github_actions/actions-91dc52575a

Author: hyperpolymath

.hypatia-baseline.json

@@ -251,12 +251,6 @@
     "type": "SD008",
     "file": "src/abi/EchidnaABI/AxiomTracker.idr"
   },
-  {
-    "severity": "critical",
-    "rule_module": "structural_drift",
-    "type": "SD008",
-    "file": "src/abi/EchidnaABI/AxiomTracker.idr"
-  },
   {
     "severity": "critical",
     "rule_module": "structural_drift",
@@ -1227,13 +1221,13 @@
     "severity": "high",
     "rule_module": "code_safety",
     "type": "unwrap_without_check",
-    "file": "src/rust/provers/mizar_ar.rs"
+    "file": "src/rust/provers/mizar.rs"
   },
   {
     "severity": "high",
     "rule_module": "code_safety",
     "type": "unwrap_without_check",
-    "file": "src/rust/provers/mizar.rs"
+    "file": "src/rust/provers/mizar_ar.rs"
   },
   {
     "severity": "high",
@@ -1371,13 +1365,13 @@
     "severity": "high",
     "rule_module": "code_safety",
     "type": "unwrap_without_check",
-    "file": "src/rust/provers/uppaal_stratego.rs"
+    "file": "src/rust/provers/uppaal.rs"
   },
   {
     "severity": "high",
     "rule_module": "code_safety",
     "type": "unwrap_without_check",
-    "file": "src/rust/provers/uppaal.rs"
+    "file": "src/rust/provers/uppaal_stratego.rs"
   },
   {
     "severity": "high",
@@ -1553,18 +1547,6 @@
     "type": "deprecated_api",
     "file": "echidna-playground/src/PlaygroundServer.res"
   },
-  {
-    "severity": "high",
-    "rule_module": "migration_rules",
-    "type": "deprecated_api",
-    "file": "echidna-playground/src/PlaygroundServer.res"
-  },
-  {
-    "severity": "high",
-    "rule_module": "migration_rules",
-    "type": "deprecated_api",
-    "file": "echidna-playground/src/Server.res"
-  },
   {
     "severity": "high",
     "rule_module": "migration_rules",
@@ -1577,36 +1559,6 @@
     "type": "deprecated_api",
     "file": "src/provers/clients/LeanTool.res"
   },
-  {
-    "severity": "high",
-    "rule_module": "migration_rules",
-    "type": "deprecated_api",
-    "file": "src/provers/clients/LeanTool.res"
-  },
-  {
-    "severity": "high",
-    "rule_module": "migration_rules",
-    "type": "deprecated_api",
-    "file": "src/provers/clients/LeanTool.res"
-  },
-  {
-    "severity": "high",
-    "rule_module": "migration_rules",
-    "type": "deprecated_api",
-    "file": "src/provers/clients/Metamath.res"
-  },
-  {
-    "severity": "high",
-    "rule_module": "migration_rules",
-    "type": "deprecated_api",
-    "file": "src/provers/clients/Metamath.res"
-  },
-  {
-    "severity": "high",
-    "rule_module": "migration_rules",
-    "type": "deprecated_api",
-    "file": "src/provers/clients/Metamath.res"
-  },
   {
     "severity": "high",
     "rule_module": "migration_rules",
@@ -1619,24 +1571,6 @@
     "type": "deprecated_api",
     "file": "src/provers/clients/SystemOnTptp.res"
   },
-  {
-    "severity": "high",
-    "rule_module": "migration_rules",
-    "type": "deprecated_api",
-    "file": "src/provers/clients/SystemOnTptp.res"
-  },
-  {
-    "severity": "high",
-    "rule_module": "migration_rules",
-    "type": "deprecated_api",
-    "file": "src/provers/clients/SystemOnTptp.res"
-  },
-  {
-    "severity": "high",
-    "rule_module": "migration_rules",
-    "type": "deprecated_api",
-    "file": "src/provers/clients/Unified.res"
-  },
   {
     "severity": "high",
     "rule_module": "migration_rules",
@@ -1655,18 +1589,6 @@
     "type": "deprecated_api",
     "file": "src/provers/clients/Wolfram.res"
   },
-  {
-    "severity": "high",
-    "rule_module": "migration_rules",
-    "type": "deprecated_api",
-    "file": "src/provers/clients/Wolfram.res"
-  },
-  {
-    "severity": "high",
-    "rule_module": "migration_rules",
-    "type": "deprecated_api",
-    "file": "src/provers/clients/Wolfram.res"
-  },
   {
     "severity": "high",
     "rule_module": "migration_rules",
@@ -1697,18 +1619,6 @@
     "type": "deprecated_api",
     "file": "src/provers/types/ProverTest.res"
   },
-  {
-    "severity": "high",
-    "rule_module": "migration_rules",
-    "type": "deprecated_api",
-    "file": "src/provers/types/ProverTest.res"
-  },
-  {
-    "severity": "high",
-    "rule_module": "migration_rules",
-    "type": "deprecated_api",
-    "file": "src/provers/utils/Http.res"
-  },
   {
     "severity": "high",
     "rule_module": "migration_rules",
@@ -1719,7 +1629,7 @@
     "severity": "high",
     "rule_module": "migration_rules",
     "type": "deprecated_api",
-    "file": "src/provers/utils/Http.res"
+    "file": "src/rescript/src/Main.res"
   },
   {
     "severity": "high",
@@ -1763,12 +1673,6 @@
     "type": "deprecated_api",
     "file": "src/rescript/src/components/TheoremSearch.res"
   },
-  {
-    "severity": "high",
-    "rule_module": "migration_rules",
-    "type": "deprecated_api",
-    "file": "src/rescript/src/Main.res"
-  },
   {
     "severity": "high",
     "rule_module": "migration_rules",
@@ -1781,6 +1685,12 @@
     "type": "download_then_run",
     "file": "mirror.yml"
   },
+  {
+    "severity": "high",
+    "rule_module": "workflow_audit",
+    "type": "missing_workflow",
+    "file": "quality.yml"
+  },
   {
     "severity": "high",
     "rule_module": "workflow_audit",

.machine_readable/6a2/AGENTIC.a2ml

@@ -189,7 +189,7 @@ can-access-training-data = true
 
 [agent-constraints]
 never-use = [
-  "believe_me, unsafeCoerce, sorry, assert_total, Admitted (Idris2 banned patterns)",
+  "believe-me, unsafeCoerce, sorry, assert_total, Admitted (Idris2 banned patterns)",
   "TypeScript, Python, Go, zig, ATS2 (banned languages)",
   "hardcoded secrets or credentials",
   "AGPL license (use MPL-2.0)",

.machine_readable/6a2/NEUROSYM.a2ml

@@ -191,11 +191,11 @@ discharge-requirements = [
 failure-action = "rollback-to-cosine (GNN model undershoots quality threshold; fall back to symbolic scoring)"
 
 [proof-obligations.abi-integrity]
-name = "Idris2 ABI proofs must contain zero believe_me or unsafeCoerce"
+name = "Idris2 ABI proofs must contain zero believe-me or unsafeCoerce"
 claim-type = "verified (trust kernel)"
 verification-method = "panic-attack scan (code-only grep, not comments)"
 discharge-requirements = [
-  "no believe_me in src/abi/*.idr",
+  "no believe-me in src/abi/*.idr",
   "no unsafeCoerce in src/idris/*.idr",
   "no Admitted except designated Parameter-axiom stubs"
 ]
@@ -241,5 +241,5 @@ scan-enabled = true
 scan-depth = "standard"
 report-format = "JSON (AssailReport)"
 proof-obligations-check = "panic-attack (code-only grep; no comments)"
-banned-patterns = ["believe_me", "unsafeCoerce", "Admitted", "sorry"]
+banned-patterns = ["believe-me", "unsafeCoerce", "Admitted", "sorry"]
 neurosym-rules-file = "standards-repo/neurosym-a2ml/hypatia-ruleset.json"

.machine_readable/6a2/STATE.a2ml

@@ -1,6 +1,10 @@
 # SPDX-License-Identifier: MPL-2.0
 # STATE.a2ml — Project state checkpoint
-# Converted from STATE.scm on 2026-03-15
+
+[manifest]
+version = "1.1"
+project = "echidna"
+type = "state-file"
 
 [metadata]
 project = "echidna"
@@ -941,7 +945,7 @@ commits = [
   "echidna 4241abf fix(provers): bounded_read_proof_file helper + 25 wrapper migrations",
   "echidna 1b613c2 fix(rest+llm): /api/v1/consult e2e wiring — env-var port + cartridge name",
 ]
-ipkg-detector-fix = "panic-attack analyze_idris now short-circuits on file_path.ends_with('.ipkg') — manifests share idr/ipkg routing but contain string-literal banned-pattern names ('zero believe_me' in package brief) that tripped substring detection. Verified: src/abi rescan drops to 0 ProofDrift findings."
+ipkg-detector-fix = "panic-attack analyze_idris now short-circuits on file_path.ends_with('.ipkg') — manifests share idr/ipkg routing but contain string-literal banned-pattern names ('zero believe-me' in package brief) that tripped substring detection. Verified: src/abi rescan drops to 0 ProofDrift findings."
 chapel-detector-fix = "panic-attack Language enum + extension map gain Chapel/.chpl. Routes through analyze_generic fallback (Chapel-specific patterns deferred — no Chapel-original code in echidna yet to dogfood). Verified: src/chapel rescan produces 6-entry AssailReport instead of erroring."
 prover-bounded-read = "src/rust/provers/io.rs ships bounded_read_proof_file with 64 MiB cap via AsyncReadExt::take(N+1) (TOCTOU-safe, errors on overflow). 25 prover backends migrated from bare tokio::fs::read_to_string. Re-scan confirms UnboundedAllocation findings 26 → 1 (only solver_integrity.rs TOML manifest read remains, separate threat shape — operator-controlled path, not a prover wrapper). 47 unflagged backends use the same pattern but already pass detector heuristic via 'limit' word presence; deferred for an estate-wide pass to avoid scope creep."
 consult-e2e-result = "Verified end-to-end up to BoJ boundary. Run echidna-rest under ECHIDNA_REST_ADDR=127.0.0.1:8765, BoJ already running on localhost:7700 in skeleton mode (cartridges_loaded=106 incl. echidna-llm-mcp). Curl POST /api/v1/consult returns: empty question → 400; valid question → 502 with 'BoJ consult returned 500 Internal Server Error' (BoJ skeleton mode self-declares invocation as placeholder). Echidna handler chain fully wired: validate → check_health → consult → POST → translate. Discovered + fixed cartridge URL bug (echidna-llm → echidna-llm-mcp) on the way."

.machine_readable/CLADE.a2ml

@@ -1,6 +1,10 @@
 # SPDX-License-Identifier: MPL-2.0
 # Clade declaration — part of the gv-clade-index registry
-# See: https://github.com/hyperpolymath/gv-clade-index
+
+[manifest]
+version = "1.1"
+project = "echidna"
+type = "clade-declaration"
 
 [identity]
 uuid = "6bab4e6b-e028-5e31-a5d8-d46c9359669b"

.machine_readable/ER.a2ml

@@ -175,7 +175,7 @@ prover-coverage = [
   "Agda:     postulate, {!!}, --type-in-type",
   "Isabelle: sorry, oops",
   "HOL4:     mk_thm (REJECT)",
-  "Idris2:   believe_me, assert_total, assert_smaller, unsafePerformIO, really_believe_me, prim__crash, unsafeCoerce",
+  "Idris2:   believe-me, assert_total, assert_smaller, unsafe-perform-io, really_believe-me, prim__crash, unsafeCoerce",
   "F*:       admit, assume",
 ]
 special-case = "scaffold-sorry lines carrying ECHIDNA_SCAFFOLD_SORRY marker are exempted from flagging (axiom:312-318)"

.machine_readable/ROADMAP.a2ml

@@ -22,7 +22,7 @@ Core invariants across all stages:
 - Trust hardening via portfolio solvers, certificate checking, and axiom tracking
 - Agentic gating (entropy budgets, explicit intent, decision recording)
 - Neurosymbolic semantics (GNN-guided search, confidence scoring, mutation testing)
-- Formal verification (Idris2 ABI proofs, zero believe_me)
+- Formal verification (Idris2 ABI proofs, zero believe-me)
 - Modularity (echidna-core as service; echidnabot as autonomous consumer; cartridges for external access)
 """
 
@@ -419,7 +419,7 @@ stage-1-requirements = [
   "✓ 3GB corpus",
   "✓ 1.43M vocab",
   "✓ Zig FFI",
-  "✓ Idris2 ABI (zero believe_me)",
+  "✓ Idris2 ABI (zero believe-me)",
   "✓ Trust pipeline (portfolio, certificates, axioms, confidence, mutation)",
   "✓ REST/gRPC/GraphQL APIs",
   "✓ A2ML conformance (AGENTIC, NEUROSYM)",

.machine_readable/agent_instructions/methodology.a2ml

@@ -73,7 +73,7 @@ deepen-not-broaden = true
 rules = [
   # Customise per project. Examples:
   # "Idris2 only for formal verification — no Lean4, Coq, Agda",
-  # "believe_me count must remain zero",
+  # "believe-me count must remain zero",
   # "FFI architecture: Idris2 → RefC → Zig → C ABI (no shortcuts)",
 ]
 

.machine_readable/ai/AI.a2ml

@@ -19,6 +19,6 @@ allow-silent-skip = false
 require-rerun-after-fix = true
 
 [forbidden-patterns]
-idris2 = ["believe_me", "assert_total", "assert_smaller", "unsafePerformIO"]
+idris2 = ["believe-me", "assert_total", "assert_smaller", "unsafe-perform-io"]
 rust-unsafe = "require SAFETY comment"
-haskell = ["unsafeCoerce", "unsafePerformIO"]
+haskell = ["unsafeCoerce", "unsafe-perform-io"]

.machine_readable/bot_directives/echidnabot.a2ml

@@ -10,6 +10,11 @@
 #   3. echidnabot's `repositories.mode` DB column
 #   4. BotMode::default() = Verifier
 
+[manifest]
+version = "1.1"
+project = "echidnabot"
+type = "bot-directive"
+
 [metadata]
 version = "1.0.0"
 last-updated = "2026-04-25"