0-AI-MANIFEST.a2ml

# 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:** MPL-2.0
- **Classification:** DUAL-USE / PRIVATE