Skip to content

Commit 86750c7

Browse files
hyperpolymathclaude
andcommitted
docs: bespoke halideiser documentation and Halide-specific ABI/FFI
Replace all template placeholders with Halide-specific content: - README.adoc: pipeline flow, Halide concepts (Func/Var/schedule), hardware targets, use cases, architecture - ROADMAP.adoc: Phase 0-6 covering parser, codegen, scheduling, auto-tuning, multi-target compilation, Idris2 proofs, ecosystem - TOPOLOGY.md: module dependency graph and data flow - Idris2 ABI: PipelineStage, SchedulePrimitive, HardwareTarget, TileSize, BufferDimension, PixelType, ValidPipeline proofs, halide_buffer_t layout - Zig FFI: pipeline context with stages/schedules/buffers, compile, execute, autotune, full test suite - 0-AI-MANIFEST.a2ml: Halide domain context and structure - .machine_readable/: STATE, META, ECOSYSTEM, ANCHOR, AI all bespoke Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 81f5fb8 commit 86750c7

18 files changed

Lines changed: 1986 additions & 748 deletions

.machine_readable/6a2/AGENTIC.a2ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
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

.machine_readable/6a2/ECOSYSTEM.a2ml

Lines changed: 23 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,12 +6,13 @@
66
(version "0.1.0")
77
(name "halideiser")
88
(type "tool")
9-
(purpose "Compile image/video pipelines to optimised Halide schedules")
9+
(purpose "Compile image/video processing pipelines to optimised Halide schedules — 10-100x speedups without Halide expertise")
1010

1111
(position-in-ecosystem
1212
(family "-iser acceleration frameworks")
1313
(meta-framework "iseriser")
1414
(relationship "sibling")
15+
(domain "image and video processing acceleration via Halide")
1516
(top-3 ("typedqliser" "chapeliser" "verisimiser")))
1617

1718
(related-projects
@@ -27,12 +28,31 @@
2728
(project "verisimiser"
2829
(relationship "sibling-priority-3")
2930
(description "VeriSimDB octad database augmentation"))
31+
(project "futharkiser"
32+
(relationship "sibling")
33+
(description "Futhark GPU array programming — complementary GPU target"))
3034
(project "squeakwell"
3135
(relationship "sibling")
3236
(description "Database recovery via constraint propagation"))
3337
(project "proven"
3438
(relationship "dependency")
35-
(description "Shared Idris2 verified library"))
39+
(description "Shared Idris2 verified library — formal proof infrastructure"))
3640
(project "typell"
3741
(relationship "dependency")
38-
(description "Type theory engine"))))
42+
(description "Type theory engine"))
43+
(project "panll"
44+
(relationship "integration")
45+
(description "Panel framework — pipeline visualisation and schedule explorer"))
46+
(project "boj-server"
47+
(relationship "integration")
48+
(description "Cartridge runtime — remote pipeline compilation")))
49+
50+
(external-dependencies
51+
(project "Halide"
52+
(relationship "upstream")
53+
(description "Image/video processing DSL by MIT/Google — algorithm/schedule separation")
54+
(url "https://halide-lang.org")
55+
(license "MIT"))
56+
(project "LLVM"
57+
(relationship "transitive-dependency")
58+
(description "Halide compiles to native code via LLVM backends"))))

.machine_readable/6a2/META.a2ml

Lines changed: 33 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -4,38 +4,54 @@
44

55
(meta
66
(version "0.1.0")
7-
(last-updated "2026-03-20")
7+
(last-updated "2026-03-21")
88

99
(architecture-decisions
1010
(adr "001-iser-pattern"
1111
(status "accepted")
12-
(context "Need to make powerful languages accessible without steep learning curves")
13-
(decision "Use manifest-driven code generation: user describes WHAT, tool generates HOW")
14-
(consequences "Users write zero target language code; all complexity in the -iser"))
12+
(context "Need to make Halide's algorithm/schedule separation accessible without Halide expertise")
13+
(decision "Use manifest-driven code generation: user describes pipeline stages in TOML, halideiser generates Halide code")
14+
(consequences "Users write zero Halide code; all complexity in the -iser; 10-100x speedups accessible to non-experts"))
1515

1616
(adr "002-abi-ffi-standard"
1717
(status "accepted")
18-
(context "Need verified interop between Rust CLI, target language, and user code")
19-
(decision "Idris2 ABI for formal proofs, Zig FFI for C-ABI bridge")
20-
(consequences "Compile-time correctness guarantees; zero runtime overhead from proofs"))
18+
(context "Need verified interop between Rust CLI, Halide C++ runtime, and user applications")
19+
(decision "Idris2 ABI for formal proofs of pipeline correctness and buffer safety; Zig FFI for C-ABI bridge")
20+
(consequences "Compile-time guarantees that buffer dimensions match between stages; zero runtime overhead from proofs"))
2121

22-
(adr "003-rsr-template"
22+
(adr "003-halide-separation"
23+
(status "accepted")
24+
(context "Halide's core insight: algorithm and schedule should be separate")
25+
(decision "Halideiser preserves this separation — pipeline stages define the algorithm, scheduling primitives define execution strategy")
26+
(consequences "Same pipeline can be compiled for different targets (CPU/GPU/WASM) by changing only the schedule"))
27+
28+
(adr "004-auto-tuning"
29+
(status "accepted")
30+
(context "Optimal schedules depend on specific hardware — cache sizes, SIMD width, GPU warp size")
31+
(decision "Implement auto-tuning: search over schedule space (tile sizes, vectorise widths, parallelism) via benchmarking")
32+
(consequences "Near-optimal performance without manual tuning; tuning results cached per (pipeline, hardware) pair"))
33+
34+
(adr "005-rsr-template"
2335
(status "accepted")
2436
(context "Need consistent project structure across 29+ -iser repos")
2537
(decision "All repos cloned from rsr-template-repo with full CI/CD and governance")
2638
(consequences "17 workflows, SECURITY.md, CONTRIBUTING, bot directives from day one")))
2739

2840
(development-practices
29-
(language "Rust" (purpose "CLI and orchestration"))
30-
(language "Idris2" (purpose "ABI formal proofs"))
31-
(language "Zig" (purpose "FFI C-ABI bridge"))
32-
(build-tool "cargo")
41+
(language "Rust" (purpose "CLI orchestration — parse, validate, generate, build, run"))
42+
(language "Idris2" (purpose "ABI formal proofs — pipeline correctness, buffer safety, schedule validity"))
43+
(language "Zig" (purpose "FFI C-ABI bridge — compiled pipeline execution from any language"))
44+
(language "C++" (purpose "Generated Halide code — Func/Var definitions and AOT compilation"))
45+
(build-tool "cargo" (purpose "Rust CLI"))
46+
(build-tool "zig build" (purpose "FFI shared/static library"))
3347
(ci "GitHub Actions (17 workflows)"))
3448

3549
(design-rationale
3650
(principle "Manifest-driven"
37-
(explanation "User intent captured in TOML; all generation is deterministic and reproducible"))
38-
(principle "Formally verified bridges"
39-
(explanation "Idris2 dependent types prove interface correctness at compile time"))
40-
(principle "Zero target language exposure"
41-
(explanation "Users never write Chapel/Julia/Futhark/etc. — the -iser handles everything"))))
51+
(explanation "Pipeline described in halideiser.toml; all generation is deterministic and reproducible"))
52+
(principle "Algorithm/Schedule separation"
53+
(explanation "Halide's core insight preserved — same algorithm runs on CPU, GPU, or WASM by changing schedule"))
54+
(principle "Formally verified buffers"
55+
(explanation "Idris2 dependent types prove buffer dimensions match between stages and bounds are respected"))
56+
(principle "Hardware-adaptive"
57+
(explanation "Auto-tuning searches the schedule space for optimal performance on specific hardware"))))

.machine_readable/6a2/NEUROSYM.a2ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
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

.machine_readable/6a2/PLAYBOOK.a2ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66

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

1111
[deployment]
1212
# method = "gitops" # gitops | manual | ci-triggered

.machine_readable/6a2/STATE.a2ml

Lines changed: 16 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -5,31 +5,35 @@
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 "halideiser")
13-
(description "Compile image/video pipelines to optimised Halide schedules")
13+
(description "Compile image/video processing pipelines to optimised Halide schedules")
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 defined, bespoke ABI/FFI/docs complete, codegen pending"))
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 "Implement halideiser.toml pipeline stage schema and parser")
25+
(step 2 "Implement Halide Func/Var codegen from parsed pipeline stages")
26+
(step 3 "Implement schedule generation with default heuristics")
27+
(step 4 "Build Idris2 ABI proofs for buffer dimensions and stage connectivity")
28+
(step 5 "Implement Zig FFI bridge for compiled pipeline execution")
29+
(step 6 "Auto-tuning loop: benchmark, perturb schedule, select fastest")
30+
(step 7 "Multi-target compilation (x86, ARM, CUDA, OpenCL, WASM)")
31+
(step 8 "Integration tests with real image processing workloads"))
2932

3033
(blockers-and-issues
3134
(none "Project is in scaffold phase — no blockers yet"))
3235

3336
(critical-next-actions
34-
(action "Implement codegen for primary use case")
35-
(action "Write first working example end-to-end")))
37+
(action "Define halideiser.toml schema for pipeline stages with buffer dimensions")
38+
(action "Implement Halide algorithm codegen from pipeline description")
39+
(action "Write first end-to-end example: blur + sharpen on a test image")))

.machine_readable/ai/AI.a2ml

Lines changed: 32 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,37 @@
1-
2-
# AI Assistant Instructions
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# AI Assistant Instructions for halideiser
33

44
## Repository Focus
5-
- `rsr-template-repo` is treated as a Rhodium Standard Repository; obey the Rhodium policies and keep `.machine_readable/` authoritative.
6-
- All machine-readable content lives under `.machine_readable/` — state files (a2ml), bot directives, and contractiles.
7-
- Prefer to keep generated files out of source control, and regenerate them with the documented commands before committing.
5+
6+
halideiser compiles image and video processing pipelines to optimised Halide
7+
schedules. It follows the hyperpolymath -iser pattern: manifest-driven code
8+
generation with Idris2 ABI proofs and Zig FFI bridge.
9+
10+
Key domain concepts:
11+
- **Func**: Halide pure function (what to compute at each pixel)
12+
- **Var**: Dimension variable (x, y, channel, frame)
13+
- **Schedule**: How to execute (tile, vectorize, parallelize, compute_at, store_at, reorder)
14+
- **buffer_t**: Strided multi-dimensional buffer (min, extent, stride per dimension)
15+
- **Auto-tuning**: Search over schedule space for optimal performance
16+
17+
## Architecture
18+
19+
- `src/manifest/` — Parse `halideiser.toml` pipeline descriptions
20+
- `src/codegen/` — Generate Halide algorithm + schedule code
21+
- `src/interface/abi/` — Idris2 proofs: PipelineStage, SchedulePrimitive, HardwareTarget, BufferDimension, TileSize
22+
- `src/interface/ffi/` — Zig FFI: pipeline context, compile, execute, autotune
23+
- `src/main.rs` — Rust CLI: init, validate, generate, build, run, info
824

925
## 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.
12-
3. After finishing edits, update STATE with your outcomes and commit with a concise, imperative message.
1326

14-
## Delivery Promises
15-
- Mention in summaries whether STATE, `.machine_readable/contractiles/`, or `.machine_readable/bot_directives/` changed.
16-
- Keep this file in sync with the repository's status; update it if the governance changes.
27+
1. Inspect `.machine_readable/6a2/STATE.a2ml` for blockers and next actions.
28+
2. Respect constraints in `.machine_readable/6a2/AGENTIC.a2ml`.
29+
3. After finishing edits, update STATE.a2ml with outcomes and commit.
30+
31+
## Key Rules
32+
33+
- All machine-readable content in `.machine_readable/` ONLY — never root.
34+
- Halide algorithm and schedule are always separate layers.
35+
- Idris2 ABI types must match Zig FFI enums exactly (tag values).
36+
- Buffer dimensions must be positive (enforced by dependent types in Idris2).
37+
- PMPL-1.0-or-later license on all original code.
Lines changed: 22 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -1,41 +1,42 @@
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-
# ANCHOR.a2ml - authoritative anchor for this repository
4+
# ANCHOR.a2ml - authoritative anchor for halideiser
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"
1212
repo = "hyperpolymath/halideiser"
1313
authority = "upstream-canonical"
1414

1515
purpose = [
16-
"Define canonical semantics and policy boundaries for this repository.",
17-
"Declare what downstream/satellite repos can extend but not redefine.",
18-
"Provide a stable golden path and invariant contract for release readiness.",
16+
"Define canonical semantics for Halide pipeline compilation.",
17+
"Declare ABI contract for pipeline stage types, scheduling primitives, and buffer layouts.",
18+
"Provide golden-path validation for generated Halide code and compiled artifacts.",
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 = "halideiser"
23+
kind = "tool"
24+
one-sentence = "Compile image/video processing pipelines to optimised Halide schedules"
25+
domain = "image-processing, video-processing, halide, acceleration"
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+
"Pipeline stage type definitions (PipelineStage, SchedulePrimitive, HardwareTarget)",
32+
"Halide buffer_t layout proofs and dimension compatibility",
33+
"Schedule generation heuristics and auto-tuning strategy",
34+
"halideiser.toml manifest schema",
3435
]
3536

3637
[implementation-policy]
37-
allowed = ["Rust", "Idris2", "Zig", "Scheme", "Shell", "Just", "AsciiDoc", "Markdown"]
38-
forbidden = ["Node.js", "npm"]
38+
allowed = ["Rust", "Idris2", "Zig", "C++", "Scheme", "Shell", "Just", "AsciiDoc", "Markdown"]
39+
forbidden = ["Node.js", "npm", "TypeScript", "Python"]
3940

4041
[golden-path]
4142
smoke-test-command = [
@@ -44,7 +45,9 @@ smoke-test-command = [
4445
]
4546

4647
success-criteria = [
47-
"Core tests pass",
48+
"Rust CLI builds and passes tests",
49+
"Zig FFI library builds and passes unit + integration tests",
50+
"Idris2 ABI type-checks with no holes",
4851
"Quality gates pass",
4952
"No unresolved critical security findings",
5053
]
@@ -56,7 +59,7 @@ must-have-anchor = true
5659
must-have-golden-path = true
5760

5861
[semantic-authority-files]
59-
language-spec = "SPECIFICATION.md"
60-
formal-proofs = "docs/proofs/PROOFS.adoc"
61-
type-theory = "docs/theory/THEORY.adoc"
62-
algorithms = "docs/theory/ALGORITHMS.adoc"
62+
formal-proofs = "src/interface/abi/"
63+
ffi-implementation = "src/interface/ffi/"
64+
manifest-schema = "src/manifest/"
65+
codegen = "src/codegen/"

0 commit comments

Comments
 (0)