-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy path0-AI-MANIFEST.a2ml
More file actions
168 lines (129 loc) · 7.64 KB
/
0-AI-MANIFEST.a2ml
File metadata and controls
168 lines (129 loc) · 7.64 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
# SPDX-License-Identifier: PMPL-1.0-or-later
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
# !! STOP - CRITICAL READING REQUIRED !!
**THIS FILE MUST BE READ FIRST BY ALL AI AGENTS**
## WHAT IS THIS?
This is the AI manifest for **ephapaxiser**. It declares:
- Canonical file locations (where things MUST be, and nowhere else)
- Critical invariants (rules that must NEVER be violated)
- Repository structure and organization
**ephapaxiser** enforces single-use linear type semantics on resources via
Ephapax. It analyses code for resource handles (file descriptors, database
connections, GPU buffers, crypto keys, session tokens), inserts Ephapax linear
type wrappers, and enforces exactly-once usage at compile time. This prevents
resource leaks, double-frees, and use-after-free bugs structurally.
## 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 -iser ecosystem, relationships
4. **AGENTIC.a2ml** - AI agent interaction patterns
5. **NEUROSYM.a2ml** - Neurosymbolic integration config (Hypatia)
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 MUST exist at:
` .machine_readable/anchors/ANCHOR.a2ml `
Do not place `ANCHOR.a2ml` at repository root.
### Maintenance Policies: `.machine_readable/policies/` ONLY
Canonical maintenance/governance files MUST exist under:
` .machine_readable/policies/ `
Minimum required files:
- `MAINTENANCE-AXES.a2ml`
- `MAINTENANCE-CHECKLIST.a2ml`
- `SOFTWARE-DEVELOPMENT-APPROACH.a2ml`
Do not place maintenance policy files in repository root.
### Bot Directives: `.machine_readable/bot_directives/` ONLY
Bot-specific instructions for automated agents (rhodibot, echidnabot, etc.).
### Contractiles: `.machine_readable/contractiles/` ONLY
Policy enforcement contracts (k9, dust, lust, must, trust).
### AI Configuration & Guides: `.machine_readable/ai/` ONLY
- `AI.a2ml` - Language-specific or LLM-specific patterns
- `PLACEHOLDERS.adoc` - Bootstrap guide
### Community & Forge Metadata: `.github/` ONLY
- `CODEOWNERS` - Review assignments
- `MAINTAINERS` - Machine-readable contact list
- `SUPPORT` - Support channels
- `SECURITY.md` - Technical security policy
- `CONTRIBUTING.md` - Technical contribution manual
- `CODE_OF_CONDUCT.md` - Conduct rules
### Agent Instructions
- `0-AI-MANIFEST.a2ml` - THIS FILE (universal entry point)
- `.claude/CLAUDE.md` - Claude Code project-specific instructions
## 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. **No stale metadata** - If root state files exist, they are OUT OF DATE
4. **License consistency** - All code PMPL-1.0-or-later unless platform requires MPL-2.0
5. **Author attribution** - Always "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"
6. **Container images** - MUST use Chainguard base (`cgr.dev/chainguard/wolfi-base:latest` or `cgr.dev/chainguard/static:latest`)
7. **Container runtime** - Podman, never Docker. Files are `Containerfile`, never `Dockerfile`
8. **Container orchestration** - `selur-compose`, never `docker-compose`
9. **Idris2 wins** - When Idris2 proofs conflict with Ephapax linear types, Idris2 always wins. The formally verified proofs are the source of truth.
10. **No dangerous patterns** - Never use `believe_me`, `assert_total`, `unsafeCoerce`, `Obj.magic`, `sorry`, or `Admitted` in any code.
## REPOSITORY STRUCTURE
This repo follows the **Dual-Track** architecture:
```
ephapaxiser/
├── 0-AI-MANIFEST.a2ml # THIS FILE (start here)
├── README.adoc # High-level orientation
├── ROADMAP.adoc # Phase plan (0-6)
├── TOPOLOGY.md # Repository structure map
├── CONTRIBUTING.adoc # Human contribution guide
├── Justfile # Task runner
├── Containerfile # OCI build (Chainguard base)
├── Cargo.toml # Rust package definition
├── LICENSE # PMPL-1.0-or-later
├── src/ # Rust source + verified interface seams
│ ├── main.rs # CLI entry point (clap)
│ ├── lib.rs # Library root
│ ├── manifest/ # ephapaxiser.toml parser
│ ├── codegen/ # Ephapax wrapper code generation
│ ├── abi/ # Rust-side ABI bindings
│ └── interface/ # Verified Interface Seams
│ ├── abi/ # Idris2 ABI — THE SPEC
│ │ ├── Types.idr # LinearResource, UsageCount, ConsumeProof
│ │ ├── Layout.idr # ResourceTracker struct layout proofs
│ │ └── Foreign.idr # FFI: analyse, wrap, consume, enforce
│ ├── ffi/ # Zig FFI — THE BRIDGE
│ │ ├── build.zig # Shared + static library build
│ │ ├── src/main.zig # C-ABI implementation
│ │ └── test/ # Integration tests
│ └── generated/ # Auto-generated C headers
├── container/ # Stapeln container ecosystem
├── docs/ # Technical documentation
├── examples/ # Usage examples
├── tests/ # Integration tests
├── verification/ # Formal verification artifacts
└── .machine_readable/ # ALL machine-readable metadata
├── 6a2/ # A2ML state files (STATE, META, ECOSYSTEM, etc.)
├── ai/ # AI configuration
├── anchors/ # Semantic boundary declarations
├── bot_directives/ # Bot instructions
├── compliance/ # REUSE dep5, cargo-deny
├── configs/ # git-cliff, etc.
├── contractiles/ # K9, must, trust, dust, lust
├── integrations/ # proven, verisimdb, vexometer
├── policies/ # Maintenance axes, checklist, SDA
└── scripts/ # Forge sync, lifecycle, verification
```
## KEY ARCHITECTURE NOTES
- **Data flow**: `ephapaxiser.toml` manifest -> resource analysis -> Idris2 ABI
proofs of linearity -> Zig FFI bridge -> Ephapax codegen -> wrapped source code
- **Idris2 ABI types**: `LinearResource`, `UsageCount`, `ResourceLifecycle`,
`ConsumeProof`, `ResourceKind`
- **Resource kinds**: FileHandle, Socket, DbConnection, GpuBuffer, CryptoKey,
SessionToken, HeapAlloc, Custom
- **Target languages**: Rust, C, Zig
- **Zero runtime overhead**: all proofs erased at compile time
## SESSION STARTUP CHECKLIST
Read THIS file (0-AI-MANIFEST.a2ml) first
Understand canonical location: `.machine_readable/`
Note invariant #9: Idris2 always wins over Ephapax when they conflict
## ATTESTATION PROOF
**"I have read the AI manifest for ephapaxiser. All machine-readable content
(state files, anchors, policies, bot directives, contractiles, AI guides) is
located in `.machine_readable/` ONLY, and community metadata is in `.github/`.
I will not create duplicate files in the root directory. I understand that
Idris2 proofs are authoritative when they conflict with Ephapax linear types."**