Skip to content

Commit 8bc8866

Browse files
hyperpolymathclaude
andcommitted
docs: bespoke architecture, roadmap, topology, and ABI definitions for atsiser
Replace all template placeholders. Architecture: C source → ATS2 linear type wrapping engine. Idris2 ABI defines LinearPtr, Viewtype, OwnershipState, AllocationSite, BufferBounds with formal proofs. Zig FFI implements C analysis, ownership graph construction, ATS2 generation, and round-trip compilation. TOPOLOGY.md documents module map and data flow. ROADMAP covers 7 phases from scaffold through ecosystem integration. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 3846282 commit 8bc8866

16 files changed

Lines changed: 1238 additions & 476 deletions

File tree

.machine_readable/6a2/AGENTIC.a2ml

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
# SPDX-License-Identifier: PMPL-1.0-or-later
22
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
33
#
4-
# AGENTIC.a2ml — AI agent constraints and capabilities
4+
# AGENTIC.a2ml — AI agent constraints and capabilities for atsiser
55
# Defines what AI agents can and cannot do in this repository.
66

77
[metadata]
88
version = "0.1.0"
9-
last-updated = "{{CURRENT_DATE}}"
9+
last-updated = "2026-03-21"
1010

1111
[agent-permissions]
1212
can-edit-source = true
@@ -17,11 +17,13 @@ can-create-files = true
1717

1818
[agent-constraints]
1919
# What AI agents must NOT do:
20-
# - Never use banned language patterns (believe_me, unsafeCoerce, etc.)
20+
# - Never use banned language patterns (believe_me, unsafeCoerce, $UNSAFE, etc.)
2121
# - Never commit secrets or credentials
2222
# - Never use banned languages (TypeScript, Python, Go, etc.)
2323
# - Never place state files in repository root (must be in .machine_readable/)
2424
# - Never use AGPL license (use PMPL-1.0-or-later)
25+
# - Never generate ATS2 code that bypasses linear type discipline
26+
# - Never emit $UNSAFE casts in generated ATS2 wrappers
2527

2628
[maintenance-integrity]
2729
fail-closed = true

.machine_readable/6a2/NEUROSYM.a2ml

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,23 @@
11
# SPDX-License-Identifier: PMPL-1.0-or-later
22
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
33
#
4-
# NEUROSYM.a2ml — Neurosymbolic integration metadata
4+
# NEUROSYM.a2ml — Neurosymbolic integration metadata for atsiser
55
# Configuration for Hypatia scanning and symbolic reasoning.
66

77
[metadata]
88
version = "0.1.0"
9-
last-updated = "{{CURRENT_DATE}}"
9+
last-updated = "2026-03-21"
1010

1111
[hypatia-config]
1212
scan-enabled = true
1313
scan-depth = "standard" # quick | standard | deep
1414
report-format = "logtalk"
1515

1616
[symbolic-rules]
17-
# Custom symbolic rules for this project
17+
# Custom symbolic rules for atsiser
1818
# - { name = "no-unsafe-ffi", pattern = "believe_me|unsafeCoerce", severity = "critical" }
19+
# - { name = "no-ats2-unsafe", pattern = "\\$UNSAFE", severity = "critical" }
20+
# - { name = "ownership-completeness", pattern = "malloc.*without.*free", severity = "warning" }
1921

2022
[neural-config]
2123
# Neural pattern detection settings

.machine_readable/6a2/PLAYBOOK.a2ml

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,25 +1,25 @@
11
# SPDX-License-Identifier: PMPL-1.0-or-later
22
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
33
#
4-
# PLAYBOOK.a2ml — Operational playbook
4+
# PLAYBOOK.a2ml — Operational playbook for atsiser
55
# Runbooks, incident response, deployment procedures.
66

77
[metadata]
88
version = "0.1.0"
9-
last-updated = "{{CURRENT_DATE}}"
9+
last-updated = "2026-03-21"
1010

1111
[deployment]
12-
# method = "gitops" # gitops | manual | ci-triggered
13-
# target = "container" # container | binary | library | wasm
12+
method = "ci-triggered"
13+
target = "binary" # Rust CLI binary + Zig shared library
1414

1515
[incident-response]
16-
# 1. Check .machine_readable/STATE.a2ml for current status
16+
# 1. Check .machine_readable/6a2/STATE.a2ml for current status
1717
# 2. Review recent commits and CI results
1818
# 3. Run `just validate` to check compliance
1919
# 4. Run `just security` to audit for vulnerabilities
2020

2121
[release-process]
22-
# 1. Update version in STATE.a2ml, META.a2ml, Justfile
22+
# 1. Update version in STATE.a2ml, META.a2ml, Cargo.toml, Justfile
2323
# 2. Run `just release-preflight` (validate + quality + security + maint-hard-pass)
2424
# 3. Optional local permission hardening: `just perms-snapshot && just perms-lock`
2525
# 4. Tag and push

.machine_readable/6a2/STATE.a2ml

Lines changed: 14 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -5,31 +5,33 @@
55
(state
66
(metadata
77
(version "0.1.0")
8-
(last-updated "2026-03-20")
8+
(last-updated "2026-03-21")
99
(author "Jonathan D.A. Jewell"))
1010

1111
(project-context
1212
(name "atsiser")
13-
(description "Wrap C codebases in ATS linear types for zero-cost memory safety")
13+
(description "Wrap C codebases in ATS2 linear types for zero-cost memory safety")
1414
(status "scaffold")
1515
(priority "—")
1616
(ecosystem "-iser family (https://github.com/hyperpolymath/iseriser)"))
1717

1818
(current-position
19-
(phase "initial-scaffold")
20-
(completion-percentage 5)
21-
(milestone "Architecture defined, CLI scaffolded, RSR template complete"))
19+
(phase "scaffold-documented")
20+
(completion-percentage 10)
21+
(milestone "Architecture documented, ABI/FFI bespoke, all placeholders replaced"))
2222

2323
(route-to-mvp
24-
(step 1 "Replace codegen stubs with target-language-specific generation")
25-
(step 2 "Implement Idris2 ABI proofs for core invariants")
26-
(step 3 "Build Zig FFI bridge")
27-
(step 4 "Integration tests with real-world examples")
28-
(step 5 "Documentation and examples"))
24+
(step 1 "C source analysis — parse headers, identify allocation patterns, track ownership")
25+
(step 2 "ATS2 wrapper generation — viewtype annotations, dataviewtype state machines")
26+
(step 3 "Proof generation — praxi/prfun obligations for ownership and bounds")
27+
(step 4 "Round-trip compilation — ATS2 → C with zero overhead verification")
28+
(step 5 "Idris2 meta-proofs — prove generated ATS2 proofs are sound")
29+
(step 6 "Ecosystem — BoJ cartridge, PanLL panels, CI/CD integration"))
2930

3031
(blockers-and-issues
3132
(none "Project is in scaffold phase — no blockers yet"))
3233

3334
(critical-next-actions
34-
(action "Implement codegen for primary use case")
35-
(action "Write first working example end-to-end")))
35+
(action "Implement C header parsing in src/core/")
36+
(action "Implement allocation pattern detection (malloc/free pairing)")
37+
(action "First working end-to-end example: simple C library → ATS2 wrapper")))

.machine_readable/ai/AI.a2ml

Lines changed: 12 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,22 @@
11

2-
# AI Assistant Instructions
2+
# AI Assistant Instructions for atsiser
33

44
## Repository Focus
5-
- `rsr-template-repo` is treated as a Rhodium Standard Repository; obey the Rhodium policies and keep `.machine_readable/` authoritative.
5+
- `atsiser` wraps C codebases in ATS2 linear types for zero-cost memory safety.
6+
- Follows the hyperpolymath -iser pattern: manifest → analysis → Idris2 ABI → Zig FFI → codegen.
67
- All machine-readable content lives under `.machine_readable/` — state files (a2ml), bot directives, and contractiles.
78
- Prefer to keep generated files out of source control, and regenerate them with the documented commands before committing.
89

10+
## Domain Knowledge
11+
- ATS2 viewtypes track pointer ownership at the type level (linear types).
12+
- `dataviewtype` encodes resource state machines (allocated → borrowed → freed).
13+
- `praxi`/`prfun` are proof-level functions — they generate zero runtime code.
14+
- Ownership graphs must be acyclic for a valid deallocation order to exist.
15+
- The Idris2 ABI layer proves meta-properties about the generated ATS2 code.
16+
917
## Workflow
10-
1. Inspect `.machine_readable/STATE.a2ml` for blockers and next actions.
11-
2. Respect any constraints listed inside `.machine_readable/AGENTIC.a2ml` when tooling changes are requested.
18+
1. Inspect `.machine_readable/6a2/STATE.a2ml` for blockers and next actions.
19+
2. Respect any constraints listed inside `.machine_readable/6a2/AGENTIC.a2ml` when tooling changes are requested.
1220
3. After finishing edits, update STATE with your outcomes and commit with a concise, imperative message.
1321

1422
## Delivery Promises

.machine_readable/anchors/ANCHOR.a2ml

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55

66
[metadata]
77
version = "1.0.0"
8-
last-updated = "{{CURRENT_DATE}}"
8+
last-updated = "2026-03-21"
99

1010
[anchor]
1111
schema = "hyperpolymath.anchor/1"
@@ -19,18 +19,19 @@ purpose = [
1919
]
2020

2121
[identity]
22-
project = "{{PROJECT_NAME}}"
23-
kind = "{{PROJECT_KIND}}" # language | library | service | tool
24-
one-sentence = "{{PROJECT_PURPOSE}}"
25-
domain = "{{PROJECT_DOMAIN}}"
22+
project = "atsiser"
23+
kind = "tool"
24+
one-sentence = "Wrap C codebases in ATS2 linear types for zero-cost memory safety"
25+
domain = "memory-safety, linear-types, C-interop, formal-verification"
2626

2727
[semantic-authority]
2828
policy = "canonical"
2929

3030
owns = [
31-
"Project semantics and specification",
32-
"Invariant definitions and contractiles",
33-
"Reference implementation behavior",
31+
"C source analysis and allocation pattern detection",
32+
"ATS2 viewtype/dataviewtype wrapper generation",
33+
"Ownership graph construction and proof obligation emission",
34+
"Round-trip ATS2-to-C compilation with zero overhead verification",
3435
]
3536

3637
[implementation-policy]

0-AI-MANIFEST.a2ml

Lines changed: 32 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,20 @@
1-
# ⚠️ STOP - CRITICAL READING REQUIRED
1+
# STOP - CRITICAL READING REQUIRED
22

33
**THIS FILE MUST BE READ FIRST BY ALL AI AGENTS**
44

55
## WHAT IS THIS?
66

7-
This is the AI manifest for **[YOUR-REPO-NAME]**. It declares:
7+
This is the AI manifest for **atsiser**. It declares:
88
- Canonical file locations (where things MUST be, and nowhere else)
99
- Critical invariants (rules that must NEVER be violated)
1010
- Repository structure and organization
1111

12+
**atsiser** wraps existing C codebases in ATS2 linear types for zero-cost
13+
memory safety. It analyses C source code, identifies memory-critical patterns
14+
(malloc/free pairs, buffer accesses, pointer arithmetic), generates ATS2
15+
wrappers with viewtype/dataviewtype annotations, and compiles them back to C
16+
with all proofs erased — zero runtime overhead.
17+
1218
## CANONICAL LOCATIONS (UNIVERSAL RULE)
1319

1420
### Machine-Readable Metadata: `.machine_readable/` ONLY
@@ -55,7 +61,7 @@ Policy enforcement contracts (k9, dust, lust, must, trust).
5561
### AI Configuration & Guides: `.machine_readable/ai/` ONLY
5662

5763
- `AI.a2ml` - Language-specific or LLM-specific patterns
58-
- `PLACEHOLDERS.md` - Bootstrap guide
64+
- `PLACEHOLDERS.adoc` - Bootstrap guide
5965

6066
### Community & Forge Metadata: `.github/` ONLY
6167

@@ -80,41 +86,47 @@ Policy enforcement contracts (k9, dust, lust, must, trust).
8086
6. **Container images** - MUST use Chainguard base (`cgr.dev/chainguard/wolfi-base:latest` or `cgr.dev/chainguard/static:latest`)
8187
7. **Container runtime** - Podman, never Docker. Files are `Containerfile`, never `Dockerfile`
8288
8. **Container orchestration** - `selur-compose`, never `docker-compose`
89+
9. **ATS2 safety** - Generated ATS2 code must never use `$UNSAFE` casts or bypass linear type discipline
8390

8491
## REPOSITORY STRUCTURE
8592

8693
This repo follows the **Dual-Track** architecture:
8794

8895
```
89-
[YOUR-REPO-NAME]/
96+
atsiser/
9097
├── 0-AI-MANIFEST.a2ml # THIS FILE (start here)
91-
├── README.adoc # High-level orientation (Rich Human)
92-
├── ROADMAP.adoc # Future direction
98+
├── README.adoc # What atsiser does, architecture, CLI commands
99+
├── ROADMAP.adoc # 7-phase roadmap (C analysis → ATS2 generation → proofs)
100+
├── TOPOLOGY.md # Module map and data flow diagram
93101
├── CONTRIBUTING.adoc # Human contribution guide
94102
├── GOVERNANCE.adoc # Decision-making model
95103
├── Justfile # Task runner
96-
├── Containerfile # OCI build
97-
├── LICENSE # Primary license
104+
├── Containerfile # OCI build (Chainguard base)
105+
├── Cargo.toml # Rust CLI dependencies
106+
├── LICENSE # PMPL-1.0-or-later
98107
├── src/ # Source code
108+
│ ├── main.rs # CLI entry point
109+
│ ├── lib.rs # Library API
110+
│ ├── manifest/ # atsiser.toml parser
111+
│ ├── codegen/ # ATS2 wrapper generation
112+
│ ├── core/ # C source analysis engine
99113
│ └── interface/ # Verified Interface Seams
100-
│ ├── abi/ # Idris2 ABI (The Spec)
101-
│ ├── ffi/ # Zig FFI (The Bridge)
102-
│ └── generated/ # C Headers (The Result)
114+
│ ├── abi/ # Idris2 ABI (proves memory safety properties)
115+
│ │ ├── Types.idr # LinearPtr, Viewtype, OwnershipState, BufferBounds
116+
│ │ ├── Layout.idr # Struct layout with per-field ownership
117+
│ │ └── Foreign.idr # C analysis + ATS2 compilation FFI
118+
│ ├── ffi/ # Zig FFI (C-ABI bridge)
119+
│ └── generated/ # Auto-generated C headers
103120
├── container/ # Stapeln container ecosystem
104-
├── docs/ # Technical depths
105-
│ ├── attribution/ # Citations, owners, maintainers (adoc)
106-
│ ├── architecture/ # Topology, diagrams
107-
│ ├── theory/ # Domain theory
108-
│ └── practice/ # Manuals
109-
├── docs/legal/ # Legal exhibits and full texts
121+
├── docs/ # Technical documentation
110122
└── .machine_readable/ # ALL machine-readable metadata
111123
```
112124

113125
## SESSION STARTUP CHECKLIST
114126

115-
Read THIS file (0-AI-MANIFEST.a2ml) first
116-
Understand canonical location: `.machine_readable/`
117-
State understanding of canonical locations
127+
Read THIS file (0-AI-MANIFEST.a2ml) first
128+
Understand canonical location: `.machine_readable/`
129+
State understanding of canonical locations
118130

119131
## ATTESTATION PROOF
120132

0 commit comments

Comments
 (0)