# STOP — CRITICAL READING REQUIRED
**THIS FILE MUST BE READ FIRST BY ALL AI AGENTS**
## WHAT IS THIS?
This is the AI manifest for **idrisiser** — the meta-prover of the -iser
family. Idrisiser takes interface definitions (OpenAPI, C headers, .proto,
type signatures) and generates Idris2 dependent-type wrappers with formal
proofs of correctness, compiled to native code via Zig FFI.
Idris2 is THE formal verification language in the hyperpolymath ecosystem.
Idrisiser is the most foundational -iser after iseriser itself.
## CANONICAL LOCATIONS (UNIVERSAL RULE)
### Machine-Readable Metadata: `.machine_readable/` 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
**CRITICAL:** If ANY of these files exist in the root directory, this is an ERROR.
### Anchor File: `.machine_readable/anchors/ANCHOR.a2ml` ONLY
Canonical authority and semantic-boundary declaration.
### Maintenance Policies: `.machine_readable/policies/` ONLY
Minimum required: MAINTENANCE-AXES.a2ml, MAINTENANCE-CHECKLIST.a2ml,
SOFTWARE-DEVELOPMENT-APPROACH.a2ml.
### Bot Directives: `.machine_readable/bot_directives/` ONLY
### Contractiles: `.machine_readable/contractiles/` ONLY
### AI Configuration: `.machine_readable/ai/` ONLY
## CORE INVARIANTS
1. **No state file duplication** — Root must NOT contain STATE.a2ml, META.a2ml, etc.
2. **Single source of truth** — `.machine_readable/` is authoritative
3. **License consistency** — All code PMPL-1.0-or-later
4. **Author attribution** — Always "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"
5. **Container images** — Chainguard base only (`cgr.dev/chainguard/`)
6. **Container runtime** — Podman, never Docker. Files are `Containerfile`.
7. **No unsafe Idris2** — Generated code must NEVER use `believe_me`, `assert_total`, or `sorry`
8. **Proof completeness** — Every proof obligation must be discharged; no holes in output
9. **ABI-FFI agreement** — Zig FFI exports must exactly match Idris2 Foreign.idr declarations
## REPOSITORY STRUCTURE
```
idrisiser/
├── 0-AI-MANIFEST.a2ml # THIS FILE (start here)
├── README.adoc # What idrisiser does, architecture, use cases
├── ROADMAP.adoc # Phase 0-6 development plan
├── TOPOLOGY.md # Module map, data flow, ecosystem position
├── Cargo.toml # Rust CLI (orchestrator)
├── src/
│ ├── main.rs # CLI: init, validate, generate, build, run, info
│ ├── lib.rs # Library API
│ ├── manifest/ # idrisiser.toml parser
│ ├── codegen/ # Idris2 + Zig code generation
│ ├── core/ # Proof obligation engine
│ ├── definitions/ # Interface definition IR
│ ├── contracts/ # Contract extraction
│ ├── errors/ # Structured diagnostics
│ ├── bridges/ # Adapters: OpenAPI, protobuf, C headers
│ └── interface/
│ ├── abi/ # Idris2 ABI (Types.idr, Layout.idr, Foreign.idr)
│ ├── ffi/ # Zig FFI (main.zig, build.zig, tests)
│ └── generated/ # Auto-generated C headers
├── verification/ # Proof verification harnesses
├── examples/ # End-to-end worked examples
└── .machine_readable/ # ALL machine-readable metadata
```
## SESSION STARTUP CHECKLIST
1. Read THIS file (0-AI-MANIFEST.a2ml) first
2. Understand canonical location: `.machine_readable/`
3. Read `.machine_readable/6a2/STATE.a2ml` for current project state
4. Read `.claude/CLAUDE.md` for project-specific patterns
## ATTESTATION PROOF
**"I have read the AI manifest for idrisiser. All machine-readable content
is located in `.machine_readable/` ONLY. I will not create duplicate files
in the root directory. I will not generate Idris2 code that uses believe_me,
assert_total, or sorry."**