docs(manifest): add ECHIDNA BoJ call-protocol snippet

Package 8: all 8 cartridge tools documented.
Protocol reference: boj-server/cartridges/echidna-llm-mcp/docs/CALL-PROTOCOL.adoc.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

0-AI-MANIFEST.a2ml

@@ -1,110 +1,102 @@
-;; SPDX-License-Identifier: PMPL-1.0-or-later
-;; Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
-;;
-;; AI Manifest — 007 Agent Meta-Language
-;; Read this file FIRST before any other file in this directory.
-
-(ai-manifest
-  (version "2.0")
-  (project "007")
-  (type "programming-language")
-  (status "active-development")
-  (license "ALL-RIGHTS-RESERVED")
-  (last-major-session "2026-03-24")
-
-  (session-resume
-    "This repo had a MAJOR session on 2026-03-24 and substantial follow-on work
-     through 2026-04. If resuming work:
-     1. Read docs/DESIGN-RATIONALE.adoc for design rationale
-     2. Read docs/AUDIT-SCORECARD-2026-03-29.md for the most recent authoritative
-        status snapshot (supersedes the 2026-03-27 scorecard)
-     3. Read TOPOLOGY.md for the current component map
-     4. Grammar is at v0.5.0 (see spec/grammar.ebnf and crates/oo7-core/src/grammar.pest)
-     5. Type checker and evaluator are substantial; L1-L3, L6-L7, L8 are solid;
-        L4 dependent types check integer bounds only; L5 refinements only on ground
-        terms; L9 proof dispatch generates obligations but does not enforce them.
-     6. Evaluator has a working agent runtime (spawn/send/receive/exchange) plus
-        five branch strategies and decision traces. Supervision restart is stubbed.
-     7. Codegen: Elixir/OTP is the best-tested path (beam_roundtrip runs the output).
-        Cranelift/QBE/WASM/Zig exist with narrower coverage.
-     8. Agent JSON API is complete (parse, validate, agent-moves, agent-card, reify).
-     9. 752 #[test] annotations in the workspace as of 2026-04-10 (CHANGELOG is catching
-        up — see 0.6.0 entry). Clippy clean on oo7-core at 0.5.0; status post-0.5.0 TBD.
-     10. Two paper drafts exist in docs/paper/. End-to-end re-reads of
-         tropical-token-types.tex found no visible math errors (prior 'KNOWN MATH ERRORS'
-         note in this manifest is retracted). Papers remain draft quality, not
-         submission-ready.
-     11. Harvard, session, and proof claims must be stated no stronger than the
-         checked artifact supports. In particular: Harvard.idr models DataExpr with
-         DAdd only; the grammar allows + - * / %. The proof generalizes trivially
-         but the generalization is not yet written down.
-     12. Use 007 dogfooding methodology (see memory/feedback_007_dogfood.md)")
-
-  (classification
-    (dual-use #t)
-    (dual-use-notice "DUAL-USE-NOTICE.adoc")
-    (visibility "private")
-    (reason "Novel agent creation language with dual-use potential"))
-
-  (description
-    "007 is a programming language for agents that make agents.
-     It enforces safety properties (no agent injection, no capability
-     escalation, no resource leaks) as core design goals. The current
-     repository is substantial but still under audit for proof, claim,
-     and release-grade alignment.")
-
-  (canonical-locations
-    (spec "spec/LANGUAGE-SPEC.adoc")
-    (grammar "spec/grammar.ebnf")
-    (examples "examples/")
-    (dual-use-notice "DUAL-USE-NOTICE.adoc"))
-
-  ;; M3 (reference type-checker oracle) has its own canonical
-  ;; documentation chain. Read these BEFORE any work on the M2/M3
-  ;; surface, because the M3 design has been re-litigated within a
-  ;; single calendar day before — see audits/audit-m3-decision.md
-  ;; revision note. The dispatch architecture document was created
-  ;; specifically to prevent that recurrence.
-  (m3-canonical-pointers
-    (architecture "audits/audit-m3-dispatch-architecture.md")
-    (decision-log "audits/audit-m3-decision.md")
-    (machine-readable-routing ".machine_readable/m3-dispatch.a2ml")
-    (v0-implementation "crates/oo7-typechecker-oracle/")
-    (v0-scope-statement "crates/oo7-typechecker-oracle/src/lib.rs")
-    (read-protocol
-      "Before modifying ANY M3-related artefact (oracle code, prover dispatch, routing, decision log):"
-      "1. Read audits/audit-m3-dispatch-architecture.md (the canonical doc)."
-      "2. Read audits/audit-m3-decision.md (the why and the sub-decisions)."
-      "3. Check .machine_readable/m3-dispatch.a2ml for the current routing."
-      "4. Run `git status` and `git diff` on the M3 surface — parallel sessions are real."
-      "5. If state has moved, re-read before writing."
-      "Violating this protocol is what created the M3-DD-3 conflict on 2026-04-13."))
-
-  (critical-invariants
-    (rule "Data expressions CANNOT contain control flow — this is grammatical, not a lint rule")
-    (rule "Capabilities are NEVER inherited — always explicit subset")
-    (rule "Agent handles are LINEAR — must be consumed exactly once")
-    (rule "Content-addressed behaviours are IMMUTABLE — referenced by hash")
-    (rule "This project is PRIVATE — do not publish or share without authorisation")
-    (rule "This project is classified as DUAL-USE — handle accordingly"))
-
-  (design-doc-conventions
-    (rule "Cite symbols, not line numbers, in design docs and audit notes.
-           Prefer `eval.rs :: ControlStmt::EnterDiscourse` or
-           `metainterpreter.rs :: MetaHook::before_step` over
-           `eval.rs:1850` / `metainterpreter.rs:1771`. Line numbers rot
-           the moment any `use` is inserted; symbol paths survive.
-           Applies to: docs/, audits/, crates/**/DESIGN-*.adoc,
-           crates/**/AUDIT-*.md. Indicative line numbers in inline code
-           comments are acceptable where the comment lives adjacent to
-           the cited site. This rule was added 2026-04-13 after the T6
-           step-semantics thread flagged citation rot as bot-hostile."))
-
-  (design-influences
-    (language "JTV" (contribution "Harvard architecture, purity, reversibility"))
-    (language "Elixir" (contribution "Actor model, supervision, distribution"))
-    (language "Chapel" (contribution "Locale-aware parallelism"))
-    (language "Ephapax" (contribution "Linear types"))
-    (language "Pony" (contribution "Capability security"))
-    (language "Unison" (contribution "Content-addressable code"))
-    (language "Chor-lambda" (contribution "Choreographic programming"))))
+# STOP - CRITICAL READING REQUIRED
+
+**THIS FILE MUST BE READ FIRST BY ALL AI AGENTS**
+
+## WHAT IS THIS?
+
+This is the AI manifest for **007-lang**. It declares:
+- Canonical file locations (where things MUST be, and nowhere else)
+- Critical invariants (rules that must NEVER be violated)
+- Repository structure and organization
+
+## CANONICAL LOCATIONS (UNIVERSAL RULE)
+
+### Machine-Readable Metadata: `.machine_readable/6a2/` ONLY
+
+These 6 A2ML files MUST exist in `.machine_readable/6a2/` directory ONLY:
+1. **STATE.a2ml** - Project state, progress, blockers
+2. **META.a2ml** - Architecture decisions, governance
+3. **ECOSYSTEM.a2ml** - Position in ecosystem, relationships
+4. **AGENTIC.a2ml** - AI agent interaction patterns
+5. **NEUROSYM.a2ml** - Neurosymbolic integration config
+6. **PLAYBOOK.a2ml** - Operational runbook
+
+### Project-Specific Canonical Pointers
+
+- **Grammar:** `spec/grammar.ebnf` and `crates/oo7-core/src/grammar.pest`
+- **Language Spec:** `spec/LANGUAGE-SPEC.adoc`
+- **Design Rationale:** `docs/DESIGN-RATIONALE.adoc`
+- **M3 Architecture:** `audits/audit-m3-dispatch-architecture.md`
+- **Dual-Use Notice:** `DUAL-USE-NOTICE.adoc`
+
+## CORE INVARIANTS
+
+1. **Harvard Architecture** - Data expressions CANNOT contain control flow. This is a grammatical invariant, not a lint rule.
+2. **Linear Handles** - Agent handles are LINEAR. They must be consumed exactly once.
+3. **No Capability Inheritance** - Capabilities are NEVER inherited; they must be an explicit subset.
+4. **Immutable Behaviors** - Content-addressed behaviors are IMMUTABLE and referenced by hash.
+5. **Privacy & Dual-Use** - This project is PRIVATE and classified as DUAL-USE. Do not share or publish without authorization.
+6. **Author Attribution** - Always "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>".
+
+## REPOSITORY STRUCTURE
+
+```
+007-lang/
+├── 0-AI-MANIFEST.a2ml         # THIS FILE (start here)
+├── README.adoc                # Project overview
+├── crates/                    # Rust workspace members
+├── proofs/                    # Idris2/Agda/Rocq proofs
+├── .machine_readable/
+│   ├── 6a2/                   # A2ML files (6 files)
+│   └── contractiles/          # MUST, TRUST, DUST, ADJUST, BUST, INTEND
+└── .bot_directives/            # Bot instructions
+```
+
+## LIFECYCLE HOOKS
+
+### on-enter (Session Start)
+
+1. Read and acknowledge this manifest.
+2. Read `.machine_readable/6a2/STATE.a2ml` for current status and blockers.
+3. State understanding of the **Harvard Architecture** invariant.
+
+### on-exit (Session End)
+
+1. Update `.machine_readable/6a2/STATE.a2ml` (v2 format).
+2. Record any new proof debt or clippy regressions.
+
+## Calling ECHIDNA via BoJ
+
+All ECHIDNA invocations go through the `echidna-llm-mcp` BoJ cartridge.
+**Never call ECHIDNA directly — always go through BoJ.**
+
+| Tool | Description |
+|------|-------------|
+| `echidna_list_provers` | Discover all 105 provers with tier/category/complexity |
+| `echidna_prove` | Invoke a prover on a file path (auto-detects from extension) |
+| `echidna_verify` | Verify inline proof content as a string |
+| `echidna_search` | Keyword search over the 66,674-proof corpus |
+| `echidna_suggest_tactics` | Advisory tactic suggestions for a goal |
+| `echidna_rank_provers` | Advisory prover ranking for a theorem |
+
+```json
+{ "tool": "echidna_list_provers", "args": {} }
+{ "tool": "echidna_prove", "args": { "file": "/path/to/proof.lean", "prover": "Lean" } }
+{ "tool": "echidna_suggest_tactics", "args": { "goal": "n + 0 = n", "prover": "Lean" } }
+```
+
+Full protocol: `boj-server/cartridges/echidna-llm-mcp/docs/CALL-PROTOCOL.adoc`
+
+## ATTESTATION PROOF
+
+After reading this file, demonstrate understanding by stating:
+
+**"I have read the AI manifest. I understand the Harvard Architecture invariant and that A2ML files are located in `.machine_readable/6a2/` ONLY."**
+
+## META
+
+- **Format Version:** 1.0.0
+- **Last Updated:** 2026-04-23
+- **Maintained By:** Jonathan D.A. Jewell (hyperpolymath)
+- **License:** PMPL-1.0-or-later
+- **Classification:** DUAL-USE / PRIVATE