Bespoke documentation: Futhark GPU compilation pipeline, Idris2 ABI types, Zig FFI

Replace all template placeholders with futharkiser-specific content:

- README.adoc: Futhark SOACs, GPU backends, architecture diagram, use cases
- ROADMAP.adoc: 7 phases from scaffold through GPU compilation to ecosystem
- Idris2 ABI: SOAC, GPUBackend, ArrayShape, MemorySpace, ParallelPattern,
  FutharkType, GPUBuffer, GPUBufferDescriptor layout (32 bytes, 8-byte aligned)
- Zig FFI: GPU context lifecycle, buffer allocation, compilation stubs,
  memory transfer, backend availability query, layout compile-time assertions
- Integration tests: lifecycle, backend query, buffer management, error handling
- TOPOLOGY.md: data flow diagram, module map, type correspondence table
- Machine-readable 6a2 files: state, meta (6 ADRs), ecosystem, agentic, neurosym, playbook
- 0-AI-MANIFEST.a2ml: futharkiser-specific invariants and repository structure

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/6a2/AGENTIC.a2ml

@@ -1,12 +1,12 @@
 # SPDX-License-Identifier: PMPL-1.0-or-later
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
-# AGENTIC.a2ml — AI agent constraints and capabilities
+# AGENTIC.a2ml — AI agent constraints and capabilities for futharkiser
 # Defines what AI agents can and cannot do in this repository.
 
 [metadata]
 version = "0.1.0"
-last-updated = "{{CURRENT_DATE}}"
+last-updated = "2026-03-21"
 
 [agent-permissions]
 can-edit-source = true
@@ -22,6 +22,8 @@ can-create-files = true
 # - Never use banned languages (TypeScript, Python, Go, etc.)
 # - Never place state files in repository root (must be in .machine_readable/)
 # - Never use AGPL license (use PMPL-1.0-or-later)
+# - Never modify Futhark SOAC definitions without updating both Idris2 ABI and Zig FFI
+# - Never change GPUBufferDescriptor layout without updating Layout.idr and main.zig simultaneously
 
 [maintenance-integrity]
 fail-closed = true

.machine_readable/6a2/ECOSYSTEM.a2ml

@@ -6,12 +6,14 @@
   (version "0.1.0")
   (name "futharkiser")
   (type "tool")
-  (purpose "Compile annotated array operations to GPU kernels via Futhark")
+  (purpose "Compile annotated array operations to GPU kernels via Futhark — identifies map/reduce/scan/scatter patterns, generates Futhark SOACs, compiles to OpenCL/CUDA/multicore GPU code")
 
   (position-in-ecosystem
     (family "-iser acceleration frameworks")
     (meta-framework "iseriser")
     (relationship "sibling")
+    (domain "GPU computing / array parallelism")
+    (target-language "Futhark (by Troels Henriksen et al., DIKU Copenhagen)")
     (top-3 ("typedqliser" "chapeliser" "verisimiser")))
 
   (related-projects
@@ -27,6 +29,9 @@
     (project "verisimiser"
       (relationship "sibling-priority-3")
       (description "VeriSimDB octad database augmentation"))
+    (project "halideiser"
+      (relationship "sibling — image processing overlap")
+      (description "Halide image processing pipeline generation; overlaps with futharkiser for image convolutions but Halide is schedule-based while Futhark is functional"))
     (project "squeakwell"
       (relationship "sibling")
       (description "Database recovery via constraint propagation"))
@@ -35,4 +40,11 @@
       (description "Shared Idris2 verified library"))
     (project "typell"
       (relationship "dependency")
-      (description "Type theory engine"))))
+      (description "Type theory engine")))
+
+  (external-dependencies
+    (project "futhark"
+      (relationship "compilation-target")
+      (url "https://futhark-lang.org")
+      (description "Purely functional array language by DIKU Copenhagen — compiles to OpenCL/CUDA GPU kernels")
+      (license "ISC"))))

.machine_readable/6a2/META.a2ml

@@ -4,38 +4,59 @@
 
 (meta
   (version "0.1.0")
-  (last-updated "2026-03-20")
+  (last-updated "2026-03-21")
 
   (architecture-decisions
     (adr "001-iser-pattern"
       (status "accepted")
-      (context "Need to make powerful languages accessible without steep learning curves")
-      (decision "Use manifest-driven code generation: user describes WHAT, tool generates HOW")
-      (consequences "Users write zero target language code; all complexity in the -iser"))
+      (context "Need to make Futhark GPU programming accessible without steep learning curves")
+      (decision "Use manifest-driven code generation: user describes WHAT array operations to accelerate, futharkiser generates Futhark SOACs and compiles to GPU kernels")
+      (consequences "Users write zero Futhark/CUDA/OpenCL code; all complexity in the -iser"))
 
     (adr "002-abi-ffi-standard"
       (status "accepted")
-      (context "Need verified interop between Rust CLI, target language, and user code")
-      (decision "Idris2 ABI for formal proofs, Zig FFI for C-ABI bridge")
-      (consequences "Compile-time correctness guarantees; zero runtime overhead from proofs"))
+      (context "Need verified interop between Rust CLI, Futhark GPU kernels, and user code")
+      (decision "Idris2 ABI for formal proofs of parallelism safety and GPU buffer layouts; Zig FFI for C-ABI bridge to Futhark runtime")
+      (consequences "Compile-time correctness guarantees for GPU memory management; zero runtime overhead from proofs"))
 
-    (adr "003-rsr-template"
+    (adr "003-futhark-soacs"
+      (status "accepted")
+      (context "Futhark's power comes from its second-order array combinators (SOACs)")
+      (decision "Map source patterns to Futhark SOACs: map, reduce, scan, scatter, flatten/unflatten")
+      (consequences "Covers the vast majority of data-parallel GPU workloads; Futhark compiler handles fusion and tiling"))
+
+    (adr "004-gpu-backends"
+      (status "accepted")
+      (context "Different users have different GPU hardware; some have no GPU at all")
+      (decision "Support all four Futhark backends: OpenCL (widest), CUDA (NVIDIA), multicore CPU, sequential C (debug)")
+      (consequences "futharkiser works everywhere, from headless servers to developer laptops"))
+
+    (adr "005-memory-space-tracking"
+      (status "accepted")
+      (context "GPU programming requires explicit management of host vs device memory")
+      (decision "Track MemorySpace (Device/Host/Shared) in the ABI type system with transfer validity proofs")
+      (consequences "Prevents invalid cross-boundary accesses at compile time; enables minimisation of host-device copies"))
+
+    (adr "006-rsr-template"
       (status "accepted")
       (context "Need consistent project structure across 29+ -iser repos")
       (decision "All repos cloned from rsr-template-repo with full CI/CD and governance")
       (consequences "17 workflows, SECURITY.md, CONTRIBUTING, bot directives from day one")))
 
   (development-practices
     (language "Rust" (purpose "CLI and orchestration"))
-    (language "Idris2" (purpose "ABI formal proofs"))
-    (language "Zig" (purpose "FFI C-ABI bridge"))
+    (language "Idris2" (purpose "ABI formal proofs — parallelism safety, GPU buffer layout verification"))
+    (language "Zig" (purpose "FFI C-ABI bridge to Futhark-compiled GPU code"))
+    (language "Futhark" (purpose "Generated target — compiled to OpenCL/CUDA GPU kernels"))
     (build-tool "cargo")
     (ci "GitHub Actions (17 workflows)"))
 
   (design-rationale
     (principle "Manifest-driven"
-      (explanation "User intent captured in TOML; all generation is deterministic and reproducible"))
+      (explanation "User intent captured in futharkiser.toml; all generation is deterministic and reproducible"))
     (principle "Formally verified bridges"
-      (explanation "Idris2 dependent types prove interface correctness at compile time"))
-    (principle "Zero target language exposure"
-      (explanation "Users never write Chapel/Julia/Futhark/etc. — the -iser handles everything"))))
+      (explanation "Idris2 dependent types prove parallelism safety (associativity of reduce operators, purity of map functions, array shape compatibility) at compile time"))
+    (principle "Zero GPU expertise required"
+      (explanation "Users never write Futhark, CUDA, or OpenCL — futharkiser generates everything from high-level array operation annotations"))
+    (principle "GPU buffer layout proofs"
+      (explanation "The ABI layer includes a GPUBufferDescriptor struct layout that is verified to match between Idris2 and Zig at compile time (32 bytes, 8-byte aligned)"))))

.machine_readable/6a2/NEUROSYM.a2ml

@@ -1,23 +1,28 @@
 # SPDX-License-Identifier: PMPL-1.0-or-later
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
-# NEUROSYM.a2ml — Neurosymbolic integration metadata
+# NEUROSYM.a2ml — Neurosymbolic integration metadata for futharkiser
 # Configuration for Hypatia scanning and symbolic reasoning.
 
 [metadata]
 version = "0.1.0"
-last-updated = "{{CURRENT_DATE}}"
+last-updated = "2026-03-21"
 
 [hypatia-config]
 scan-enabled = true
 scan-depth = "standard"  # quick | standard | deep
 report-format = "logtalk"
 
 [symbolic-rules]
-# Custom symbolic rules for this project
+# Custom symbolic rules for futharkiser:
+# - Verify SOAC enum values match between Idris2 Types.idr and Zig main.zig
+# - Verify GPUBufferDescriptor layout (32 bytes, 8-byte aligned) in both layers
+# - Verify MemorySpace enum values (Device=0, Host=1, Shared=2) are consistent
 # - { name = "no-unsafe-ffi", pattern = "believe_me|unsafeCoerce", severity = "critical" }
+# - { name = "soac-consistency", pattern = "SOAC mismatch", severity = "high" }
 
 [neural-config]
-# Neural pattern detection settings
+# Neural pattern detection for array-parallel code:
 # confidence-threshold = 0.85
 # model = "hypatia-v2"
+# detect-patterns = ["map", "reduce", "scan", "scatter", "stencil"]

.machine_readable/6a2/PLAYBOOK.a2ml

@@ -1,25 +1,27 @@
 # SPDX-License-Identifier: PMPL-1.0-or-later
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
-# PLAYBOOK.a2ml — Operational playbook
+# PLAYBOOK.a2ml — Operational playbook for futharkiser
 # Runbooks, incident response, deployment procedures.
 
 [metadata]
 version = "0.1.0"
-last-updated = "{{CURRENT_DATE}}"
+last-updated = "2026-03-21"
 
 [deployment]
-# method = "gitops"  # gitops | manual | ci-triggered
-# target = "container"  # container | binary | library | wasm
+method = "ci-triggered"
+target = "binary"  # Rust CLI binary + Zig shared library
+# Future: container target once Futhark runtime is integrated
 
 [incident-response]
-# 1. Check .machine_readable/STATE.a2ml for current status
+# 1. Check .machine_readable/6a2/STATE.a2ml for current status
 # 2. Review recent commits and CI results
 # 3. Run `just validate` to check compliance
 # 4. Run `just security` to audit for vulnerabilities
+# 5. Verify Idris2 ABI and Zig FFI are in sync (GPUBufferDescriptor layout, Result codes)
 
 [release-process]
-# 1. Update version in STATE.a2ml, META.a2ml, Justfile
+# 1. Update version in STATE.a2ml, META.a2ml, Cargo.toml, main.zig VERSION constant
 # 2. Run `just release-preflight` (validate + quality + security + maint-hard-pass)
 # 3. Optional local permission hardening: `just perms-snapshot && just perms-lock`
 # 4. Tag and push

.machine_readable/6a2/STATE.a2ml

@@ -5,31 +5,34 @@
 (state
   (metadata
     (version "0.1.0")
-    (last-updated "2026-03-20")
+    (last-updated "2026-03-21")
     (author "Jonathan D.A. Jewell"))
 
   (project-context
     (name "futharkiser")
     (description "Compile annotated array operations to GPU kernels via Futhark")
-    (status "scaffold")
+    (status "scaffold — documentation bespoked")
     (priority "—")
     (ecosystem "-iser family (https://github.com/hyperpolymath/iseriser)"))
 
   (current-position
     (phase "initial-scaffold")
-    (completion-percentage 5)
-    (milestone "Architecture defined, CLI scaffolded, RSR template complete"))
+    (completion-percentage 10)
+    (milestone "Architecture defined, CLI scaffolded, RSR template complete, Idris2 ABI types bespoked (SOAC, GPUBackend, ArrayShape, MemorySpace, ParallelPattern), Zig FFI bespoked with GPU buffer management, documentation updated"))
 
   (route-to-mvp
-    (step 1 "Replace codegen stubs with target-language-specific generation")
-    (step 2 "Implement Idris2 ABI proofs for core invariants")
-    (step 3 "Build Zig FFI bridge")
-    (step 4 "Integration tests with real-world examples")
-    (step 5 "Documentation and examples"))
+    (step 1 "Implement pattern detection — identify map/reduce/scan/scatter in source code")
+    (step 2 "Implement Futhark codegen — generate .fut files from detected patterns")
+    (step 3 "Integrate Futhark compiler invocation (futhark opencl/cuda/multicore/c)")
+    (step 4 "GPU buffer allocation and host<->device memory transfer via Zig FFI")
+    (step 5 "Idris2 proofs of parallelism safety (associativity, purity, shape compatibility)")
+    (step 6 "First end-to-end example: vector addition on GPU via OpenCL backend")
+    (step 7 "Benchmarks against hand-written CUDA/OpenCL"))
 
   (blockers-and-issues
     (none "Project is in scaffold phase — no blockers yet"))
 
   (critical-next-actions
-    (action "Implement codegen for primary use case")
-    (action "Write first working example end-to-end")))
+    (action "Implement source-level pattern detection for map/reduce/scan")
+    (action "Generate first .fut Futhark program from detected patterns")
+    (action "Invoke futhark compiler and link generated C library")))

0-AI-MANIFEST.a2ml

@@ -1,19 +1,26 @@
-# ⚠️ STOP - CRITICAL READING REQUIRED
+# STOP - CRITICAL READING REQUIRED
 
 **THIS FILE MUST BE READ FIRST BY ALL AI AGENTS**
 
 ## WHAT IS THIS?
 
-This is the AI manifest for **[YOUR-REPO-NAME]**. It declares:
+This is the AI manifest for **futharkiser**. It declares:
 - Canonical file locations (where things MUST be, and nowhere else)
 - Critical invariants (rules that must NEVER be violated)
 - Repository structure and organization
 
+**futharkiser** compiles annotated array operations to GPU kernels via Futhark.
+It identifies array-parallel patterns (map, reduce, scan, scatter) in source code,
+generates Futhark programs using second-order array combinators (SOACs), and compiles
+them to OpenCL/CUDA/multicore GPU code via the Futhark compiler. The Idris2 ABI layer
+formally proves parallelism safety and correct GPU buffer layouts. The Zig FFI layer
+provides the C-ABI bridge between the host application and Futhark-compiled kernels.
+
 ## CANONICAL LOCATIONS (UNIVERSAL RULE)
 
 ### Machine-Readable Metadata: `.machine_readable/` ONLY
 
-These 6 a2ml files MUST exist in `.machine_readable/` directory 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
@@ -46,7 +53,7 @@ Do not place maintenance policy files in repository root.
 
 ### Bot Directives: `.machine_readable/bot_directives/` ONLY
 
-Bot-specific instructions for your automated agents.
+Bot-specific instructions for automated agents.
 
 ### Contractiles: `.machine_readable/contractiles/` ONLY
 
@@ -55,7 +62,7 @@ Policy enforcement contracts (k9, dust, lust, must, trust).
 ### AI Configuration & Guides: `.machine_readable/ai/` ONLY
 
 - `AI.a2ml` - Language-specific or LLM-specific patterns
-- `PLACEHOLDERS.md` - Bootstrap guide
+- `PLACEHOLDERS.adoc` - Bootstrap guide
 
 ### Community & Forge Metadata: `.github/` ONLY
 
@@ -80,42 +87,50 @@ Policy enforcement contracts (k9, dust, lust, must, trust).
 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. **Futhark specifics** - SOACs are map/reduce/scan/scatter; GPU backends are OpenCL/CUDA/multicore/sequential
+10. **ABI/FFI contract** - Idris2 Types.idr defines the domain types (SOAC, GPUBackend, ArrayShape, MemorySpace, ParallelPattern); Zig main.zig must match these exactly
 
 ## REPOSITORY STRUCTURE
 
 This repo follows the **Dual-Track** architecture:
 
 ```
-[YOUR-REPO-NAME]/
+futharkiser/
 ├── 0-AI-MANIFEST.a2ml         # THIS FILE (start here)
 ├── README.adoc                 # High-level orientation (Rich Human)
-├── ROADMAP.adoc                # Future direction
+├── ROADMAP.adoc                # Phased roadmap (scaffold → GPU compilation → proofs)
 ├── CONTRIBUTING.adoc           # Human contribution guide
-├── GOVERNANCE.adoc             # Decision-making model
-├── Justfile                    # Task runner
+├── Cargo.toml                  # Rust CLI build
 ├── Containerfile               # OCI build
-├── LICENSE                     # Primary license
-├── src/                        # Source code
+├── LICENSE                     # PMPL-1.0-or-later
+├── src/
+│   ├── main.rs                 # CLI entry point (init, validate, generate, build, run)
+│   ├── lib.rs                  # Library API
+│   ├── manifest/mod.rs         # futharkiser.toml parser
+│   ├── codegen/mod.rs          # Futhark code generation from detected patterns
 │   └── interface/              # Verified Interface Seams
-│       ├── abi/                # Idris2 ABI (The Spec)
-│       ├── ffi/                # Zig FFI (The Bridge)
-│       └── generated/          # C Headers (The Result)
+│       ├── abi/                # Idris2 ABI (formal proofs of parallelism safety)
+│       │   ├── Types.idr       # SOAC, GPUBackend, ArrayShape, MemorySpace, etc.
+│       │   ├── Layout.idr      # GPU buffer descriptor layout proofs
+│       │   └── Foreign.idr     # FFI declarations (compile, execute, alloc_buffer)
+│       ├── ffi/                # Zig FFI (C-ABI bridge to Futhark runtime)
+│       │   ├── build.zig       # Build config for libfutharkiser
+│       │   ├── src/main.zig    # FFI implementation
+│       │   └── test/           # Integration tests
+│       └── generated/          # Auto-generated C headers
 ├── container/                  # Stapeln container ecosystem
-├── docs/                       # Technical depths
-│   ├── attribution/            # Citations, owners, maintainers (adoc)
-│   ├── architecture/           # Topology, diagrams
-│   ├── theory/                 # Domain theory
-│   └── practice/               # Manuals
-├── docs/legal/                  # Legal exhibits and full texts
+├── docs/                       # Technical documentation
 └── .machine_readable/          # ALL machine-readable metadata
+    └── 6a2/                    # STATE, META, ECOSYSTEM, AGENTIC, NEUROSYM, PLAYBOOK
 ```
 
 ## SESSION STARTUP CHECKLIST
 
-✅ Read THIS file (0-AI-MANIFEST.a2ml) first
-✅ Understand canonical location: `.machine_readable/`
-✅ State understanding of canonical locations
+1. Read THIS file (0-AI-MANIFEST.a2ml) first
+2. Understand canonical location: `.machine_readable/`
+3. State understanding of canonical locations
+4. Read `.machine_readable/6a2/STATE.a2ml` for current project state
 
 ## ATTESTATION PROOF
 
-**"I have read the AI manifest. 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 have read the AI manifest for futharkiser. 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."**