diff --git a/CODE_OF_CONDUCT.adoc b/CODE_OF_CONDUCT.adoc new file mode 100644 index 0000000..bd2a83c --- /dev/null +++ b/CODE_OF_CONDUCT.adoc @@ -0,0 +1,24 @@ +== Contributor Covenant Code of Conduct + +=== Our Pledge + +We pledge to make participation a harassment-free experience for +everyone. + +=== Our Standards + +*Positive behavior:* * Using welcoming language * Being respectful of +differing viewpoints * Accepting constructive criticism * Focusing on +what is best for the community + +*Unacceptable behavior:* * Harassment, trolling, or personal attacks * +Publishing private information without permission + +=== Enforcement + +Report issues to the maintainers. All complaints will be reviewed. + +=== Attribution + +Adapted from https://www.contributor-covenant.org/[Contributor Covenant] +v2.1. diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md deleted file mode 100644 index caeda1c..0000000 --- a/CODE_OF_CONDUCT.md +++ /dev/null @@ -1,27 +0,0 @@ - -# Contributor Covenant Code of Conduct - -## Our Pledge - -We pledge to make participation a harassment-free experience for everyone. - -## Our Standards - -**Positive behavior:** -* Using welcoming language -* Being respectful of differing viewpoints -* Accepting constructive criticism -* Focusing on what is best for the community - -**Unacceptable behavior:** -* Harassment, trolling, or personal attacks -* Publishing private information without permission - -## Enforcement - -Report issues to the maintainers. All complaints will be reviewed. - -## Attribution - -Adapted from [Contributor Covenant](https://www.contributor-covenant.org/) v2.1. - diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc new file mode 100644 index 0000000..858f44f --- /dev/null +++ b/CONTRIBUTING.adoc @@ -0,0 +1,71 @@ +== Contributing + +Thank you for your interest in contributing! We follow a "`Dual-Track`" +architecture where human-readable documentation lives in the root and +machine-readable policies live in `+.machine_readable/+`. + +=== How to Contribute + +We welcome contributions in many forms: + +* *Code:* Improving the core stack or extensions +* *Documentation:* Enhancing docs or AI manifests +* *Testing:* Adding property-based tests or formal proofs +* *Bug reports:* Filing clear, reproducible issues + +=== Getting Started + +[arabic] +. *Read the AI Manifest:* Start with `+0-AI-MANIFEST.a2ml+` (if present) +to understand the repository structure. +. *Environment:* Use `+nix develop+` or `+direnv allow+` to set up your +tools. +. *Task Runner:* Use `+just+` to see available commands +(`+just --list+`). + +=== Development Workflow + +==== Branch Naming + +.... +docs/short-description # Documentation +test/what-added # Test additions +feat/short-description # New features +fix/issue-number-description # Bug fixes +refactor/what-changed # Code improvements +security/what-fixed # Security fixes +.... + +==== Commit Messages + +We follow https://www.conventionalcommits.org/[Conventional Commits]: + +.... +(): + +[optional body] + +[optional footer] +.... + +Types: `+feat+`, `+fix+`, `+docs+`, `+test+`, `+refactor+`, `+ci+`, +`+chore+`, `+security+` + +=== Reporting Bugs + +Before reporting: 1. Search existing issues 2. Check if it’s already +fixed in `+main+` + +When reporting, include: - Clear, descriptive title - Environment +details (OS, versions, toolchain) - Steps to reproduce - Expected vs +actual behaviour + +=== Code of Conduct + +All contributors are expected to adhere to our +link:CODE_OF_CONDUCT.md[Code of Conduct]. + +=== License + +By contributing, you agree that your contributions will be licensed +under the same license as the project (see LICENSE). diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md deleted file mode 100644 index 80ecdac..0000000 --- a/CONTRIBUTING.md +++ /dev/null @@ -1,66 +0,0 @@ - -# Contributing - -Thank you for your interest in contributing! We follow a "Dual-Track" architecture where human-readable documentation lives in the root and machine-readable policies live in `.machine_readable/`. - -## How to Contribute - -We welcome contributions in many forms: - -- **Code:** Improving the core stack or extensions -- **Documentation:** Enhancing docs or AI manifests -- **Testing:** Adding property-based tests or formal proofs -- **Bug reports:** Filing clear, reproducible issues - -## Getting Started - -1. **Read the AI Manifest:** Start with `0-AI-MANIFEST.a2ml` (if present) to understand the repository structure. -2. **Environment:** Use `nix develop` or `direnv allow` to set up your tools. -3. **Task Runner:** Use `just` to see available commands (`just --list`). - -## Development Workflow - -### Branch Naming - -``` -docs/short-description # Documentation -test/what-added # Test additions -feat/short-description # New features -fix/issue-number-description # Bug fixes -refactor/what-changed # Code improvements -security/what-fixed # Security fixes -``` - -### Commit Messages - -We follow [Conventional Commits](https://www.conventionalcommits.org/): - -``` -(): - -[optional body] - -[optional footer] -``` - -Types: `feat`, `fix`, `docs`, `test`, `refactor`, `ci`, `chore`, `security` - -## Reporting Bugs - -Before reporting: -1. Search existing issues -2. Check if it's already fixed in `main` - -When reporting, include: -- Clear, descriptive title -- Environment details (OS, versions, toolchain) -- Steps to reproduce -- Expected vs actual behaviour - -## Code of Conduct - -All contributors are expected to adhere to our [Code of Conduct](CODE_OF_CONDUCT.md). - -## License - -By contributing, you agree that your contributions will be licensed under the same license as the project (see [LICENSE](LICENSE)). diff --git a/SECURITY.md b/SECURITY.adoc similarity index 57% rename from SECURITY.md rename to SECURITY.adoc index 89d9e4d..02f95f9 100644 --- a/SECURITY.md +++ b/SECURITY.adoc @@ -1,21 +1,24 @@ -# Security Policy +== Security Policy -## Supported Versions +=== Supported Versions -| Version | Supported | -|---------|-----------| -| 0.1.x | ✅ | +[cols=",",options="header",] +|=== +|Version |Supported +|0.1.x |✅ +|=== -## Reporting a Vulnerability +=== Reporting a Vulnerability Please report security vulnerabilities to: j.d.a.jewell@open.ac.uk Do NOT open a public issue for security vulnerabilities. -## Response Time +=== Response Time -We aim to respond within 48 hours and provide a fix within 7 days for critical issues. +We aim to respond within 48 hours and provide a fix within 7 days for +critical issues. -## Scope +=== Scope This policy covers the ponyiser CLI tool and its generated artifacts. diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc new file mode 100644 index 0000000..d9b31fa --- /dev/null +++ b/TEST-NEEDS.adoc @@ -0,0 +1,36 @@ +== TEST-NEEDS.md — ponyiser + +=== CRG Grade: C — ACHIEVED 2026-04-04 + +=== Current Test State + +[width="100%",cols="42%,29%,29%",options="header",] +|=== +|Category |Count |Notes +|Integration tests (Rust) |1 |`+tests/integration_tests.rs+` + +|Verification tests |Unit-level |`+verification/tests/+` directory +present + +|FFI tests |Present |`+src/interface/ffi/test/+` +|=== + +=== What’s Covered + +* [x] Integration test framework +* [x] FFI verification layer +* [x] Aspect-based organization + +=== Still Missing (for CRG B+) + +* [ ] Property-based testing (proptest) +* [ ] Fuzzing targets +* [ ] Performance benchmarks +* [ ] Platform-specific test matrix + +=== Run Tests + +[source,bash] +---- +cd /var/mnt/eclipse/repos/ponyiser && cargo test +---- diff --git a/TEST-NEEDS.md b/TEST-NEEDS.md deleted file mode 100644 index b8097c2..0000000 --- a/TEST-NEEDS.md +++ /dev/null @@ -1,30 +0,0 @@ -# TEST-NEEDS.md — ponyiser - -## CRG Grade: C — ACHIEVED 2026-04-04 - -## Current Test State - -| Category | Count | Notes | -|----------|-------|-------| -| Integration tests (Rust) | 1 | `tests/integration_tests.rs` | -| Verification tests | Unit-level | `verification/tests/` directory present | -| FFI tests | Present | `src/interface/ffi/test/` | - -## What's Covered - -- [x] Integration test framework -- [x] FFI verification layer -- [x] Aspect-based organization - -## Still Missing (for CRG B+) - -- [ ] Property-based testing (proptest) -- [ ] Fuzzing targets -- [ ] Performance benchmarks -- [ ] Platform-specific test matrix - -## Run Tests - -```bash -cd /var/mnt/eclipse/repos/ponyiser && cargo test -``` diff --git a/TOPOLOGY.md b/TOPOLOGY.adoc similarity index 71% rename from TOPOLOGY.md rename to TOPOLOGY.adoc index 067ab1b..cc9b377 100644 --- a/TOPOLOGY.md +++ b/TOPOLOGY.adoc @@ -1,14 +1,19 @@ - - -# TOPOLOGY.md — ponyiser +== TOPOLOGY.md — ponyiser -## Purpose +=== Purpose -ponyiser eliminates data races by wrapping concurrent code in Pony actor and behaviour wrappers with reference capability annotations. Pony's six reference capabilities (iso, val, ref, box, trn, tag) guarantee data-race freedom at compile time without locks or runtime checks. ponyiser reads concurrency patterns from a `ponyiser.toml` manifest and generates Pony actor wrappers with the appropriate capability annotations, targeting any codebase that needs provably safe concurrency. +ponyiser eliminates data races by wrapping concurrent code in Pony actor +and behaviour wrappers with reference capability annotations. Pony’s six +reference capabilities (iso, val, ref, box, trn, tag) guarantee +data-race freedom at compile time without locks or runtime checks. +ponyiser reads concurrency patterns from a `+ponyiser.toml+` manifest +and generates Pony actor wrappers with the appropriate capability +annotations, targeting any codebase that needs provably safe +concurrency. -## Module Map +=== Module Map -``` +.... ponyiser/ ├── src/ │ ├── main.rs # CLI entry point (clap): init, validate, generate, build, run, info @@ -20,11 +25,11 @@ ponyiser/ ├── verification/ # Proof harnesses ├── container/ # Stapeln container ecosystem └── .machine_readable/ # A2ML metadata -``` +.... -## Data Flow +=== Data Flow -``` +.... ponyiser.toml manifest │ ┌────▼────┐ @@ -43,4 +48,4 @@ ponyiser.toml manifest ┌────▼────┐ │ Ponyc │ compile-time verification of reference capabilities └─────────┘ -``` +.... diff --git a/docs/architecture/TOPOLOGY.adoc b/docs/architecture/TOPOLOGY.adoc new file mode 100644 index 0000000..7cf23cf --- /dev/null +++ b/docs/architecture/TOPOLOGY.adoc @@ -0,0 +1,121 @@ +== Ponyiser Topology + +=== Overview + +Ponyiser wraps concurrent code in Pony reference capabilities for +compile-time data-race freedom. It follows the hyperpolymath -iser +architecture: TOML manifest in, capability-safe Pony actors out. + +=== Data Flow + +.... +ponyiser.toml Rust CLI Pony Codegen +(user manifest) --> (parse + validate) --> (actors + behaviours) + | | + v v + Capability Inference Zig FFI Bridge + (assign iso/val/ref/ (C-ABI interop with + box/trn/tag) existing code) + | | + v v + Idris2 ABI Proofs Generated Output + (subtyping lattice, (Pony source + + sendability, FFI bridge + + mailbox layout) C headers) +.... + +=== Module Map + +[width="100%",cols="30%,37%,33%",options="header",] +|=== +|Module |Language |Purpose +|`+src/main.rs+` |Rust |CLI entry point (init, validate, generate, +build, run) + +|`+src/lib.rs+` |Rust |Library API + +|`+src/manifest/+` |Rust |Parse and validate `+ponyiser.toml+` + +|`+src/codegen/+` |Rust |Generate Pony actors, behaviours, capability +annotations + +|`+src/abi/+` |Rust |Runtime types mirroring Idris2 ABI definitions + +|`+src/interface/abi/Types.idr+` |Idris2 |RefCapability, Actor, +Behaviour, CausalMessage, CapabilitySubtyping + +|`+src/interface/abi/Layout.idr+` |Idris2 |Actor mailbox layout, +capability-annotated fields, C ABI proofs + +|`+src/interface/abi/Foreign.idr+` |Idris2 |FFI declarations: capability +inference, subtyping, sendability, codegen + +|`+src/interface/ffi/src/main.zig+` |Zig |FFI implementation: capability +lattice, sendability, actor codegen + +|`+src/interface/ffi/build.zig+` |Zig |Build configuration for +shared/static library + +|`+src/interface/ffi/test/+` |Zig |Integration tests for capability +subtyping and sendability +|=== + +=== Capability Subtyping Lattice + +.... + iso + / \ + trn val + | | + ref | + \ / + box + | + tag +.... + +* *iso* (top): isolated, exclusive read/write, sendable (consumed) +* *trn*: transitional, write with read-only aliases, consumed into val +* *val*: immutable, globally shareable, sendable +* *ref*: mutable, actor-local only +* *box*: read-only, actor-local +* *tag* (bottom): identity-only, always sendable + +Sendable across actors: iso (consumed), val, tag. Actor-local only: ref, +box, trn. + +=== Actor Architecture + +.... ++-------------------+ causal messages +-------------------+ +| Actor A | ----------------------> | Actor B | +| (private heap) | (iso/val/tag only) | (private heap) | +| | | | +| fields: | | behaviours: | +| config: val | | on_receive( | +| state: ref | | data: iso, | +| logger: tag | | cfg: val | ++-------------------+ | ) | + +-------------------+ +.... + +=== Verification Layers + +[arabic] +. *Idris2 ABI* — proves capability subtyping lattice and sendability at +the type level +. *Zig FFI* — runtime checks matching the Idris2 proofs, with +comprehensive tests +. *Rust CLI* — validates manifest, invokes inference and codegen +. *Generated Pony* — Pony compiler itself enforces capabilities on the +output + +=== Integration Points + +* *iseriser*: meta-framework that generates -iser scaffolding +* *proven*: shared Idris2 verified library (potential capability proof +sharing) +* *typell*: type theory engine (capability lattice expressible in +TypeLL) +* *PanLL*: capability analysis panel, actor graph visualiser +* *BoJ-server*: cartridge for ponyiser operations diff --git a/docs/architecture/TOPOLOGY.md b/docs/architecture/TOPOLOGY.md deleted file mode 100644 index b46992f..0000000 --- a/docs/architecture/TOPOLOGY.md +++ /dev/null @@ -1,98 +0,0 @@ - - - -# Ponyiser Topology - -## Overview - -Ponyiser wraps concurrent code in Pony reference capabilities for compile-time -data-race freedom. It follows the hyperpolymath -iser architecture: TOML -manifest in, capability-safe Pony actors out. - -## Data Flow - -``` -ponyiser.toml Rust CLI Pony Codegen -(user manifest) --> (parse + validate) --> (actors + behaviours) - | | - v v - Capability Inference Zig FFI Bridge - (assign iso/val/ref/ (C-ABI interop with - box/trn/tag) existing code) - | | - v v - Idris2 ABI Proofs Generated Output - (subtyping lattice, (Pony source + - sendability, FFI bridge + - mailbox layout) C headers) -``` - -## Module Map - -| Module | Language | Purpose | -|--------|----------|---------| -| `src/main.rs` | Rust | CLI entry point (init, validate, generate, build, run) | -| `src/lib.rs` | Rust | Library API | -| `src/manifest/` | Rust | Parse and validate `ponyiser.toml` | -| `src/codegen/` | Rust | Generate Pony actors, behaviours, capability annotations | -| `src/abi/` | Rust | Runtime types mirroring Idris2 ABI definitions | -| `src/interface/abi/Types.idr` | Idris2 | RefCapability, Actor, Behaviour, CausalMessage, CapabilitySubtyping | -| `src/interface/abi/Layout.idr` | Idris2 | Actor mailbox layout, capability-annotated fields, C ABI proofs | -| `src/interface/abi/Foreign.idr` | Idris2 | FFI declarations: capability inference, subtyping, sendability, codegen | -| `src/interface/ffi/src/main.zig` | Zig | FFI implementation: capability lattice, sendability, actor codegen | -| `src/interface/ffi/build.zig` | Zig | Build configuration for shared/static library | -| `src/interface/ffi/test/` | Zig | Integration tests for capability subtyping and sendability | - -## Capability Subtyping Lattice - -``` - iso - / \ - trn val - | | - ref | - \ / - box - | - tag -``` - -- **iso** (top): isolated, exclusive read/write, sendable (consumed) -- **trn**: transitional, write with read-only aliases, consumed into val -- **val**: immutable, globally shareable, sendable -- **ref**: mutable, actor-local only -- **box**: read-only, actor-local -- **tag** (bottom): identity-only, always sendable - -Sendable across actors: iso (consumed), val, tag. -Actor-local only: ref, box, trn. - -## Actor Architecture - -``` -+-------------------+ causal messages +-------------------+ -| Actor A | ----------------------> | Actor B | -| (private heap) | (iso/val/tag only) | (private heap) | -| | | | -| fields: | | behaviours: | -| config: val | | on_receive( | -| state: ref | | data: iso, | -| logger: tag | | cfg: val | -+-------------------+ | ) | - +-------------------+ -``` - -## Verification Layers - -1. **Idris2 ABI** — proves capability subtyping lattice and sendability at the type level -2. **Zig FFI** — runtime checks matching the Idris2 proofs, with comprehensive tests -3. **Rust CLI** — validates manifest, invokes inference and codegen -4. **Generated Pony** — Pony compiler itself enforces capabilities on the output - -## Integration Points - -- **iseriser**: meta-framework that generates -iser scaffolding -- **proven**: shared Idris2 verified library (potential capability proof sharing) -- **typell**: type theory engine (capability lattice expressible in TypeLL) -- **PanLL**: capability analysis panel, actor graph visualiser -- **BoJ-server**: cartridge for ponyiser operations diff --git a/llm-warmup-dev.adoc b/llm-warmup-dev.adoc new file mode 100644 index 0000000..fce4530 --- /dev/null +++ b/llm-warmup-dev.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — ponyiser (Developer) + +=== What is ponyiser? + +See README.adoc for overview. + +=== Key Commands + +* `+just setup+` — set up development environment +* `+just build+` — build the project +* `+just test+` — run tests +* `+just doctor+` — diagnose issues +* `+just heal+` — attempt auto-repair + +=== Quick Context + +* License: MPL-2.0 +* Part of hyperpolymath ecosystem +* See EXPLAINME.adoc for architecture diff --git a/llm-warmup-dev.md b/llm-warmup-dev.md deleted file mode 100644 index 5d07ce0..0000000 --- a/llm-warmup-dev.md +++ /dev/null @@ -1,16 +0,0 @@ -# LLM Warmup — ponyiser (Developer) - -## What is ponyiser? -See README.adoc for overview. - -## Key Commands -- `just setup` — set up development environment -- `just build` — build the project -- `just test` — run tests -- `just doctor` — diagnose issues -- `just heal` — attempt auto-repair - -## Quick Context -- License: MPL-2.0 -- Part of hyperpolymath ecosystem -- See EXPLAINME.adoc for architecture diff --git a/llm-warmup-user.adoc b/llm-warmup-user.adoc new file mode 100644 index 0000000..26cc440 --- /dev/null +++ b/llm-warmup-user.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — ponyiser (User) + +=== What is ponyiser? + +See README.adoc for overview. + +=== Key Commands + +* `+just setup+` — set up development environment +* `+just build+` — build the project +* `+just test+` — run tests +* `+just doctor+` — diagnose issues +* `+just heal+` — attempt auto-repair + +=== Quick Context + +* License: MPL-2.0 +* Part of hyperpolymath ecosystem +* See EXPLAINME.adoc for architecture diff --git a/llm-warmup-user.md b/llm-warmup-user.md deleted file mode 100644 index 714ba12..0000000 --- a/llm-warmup-user.md +++ /dev/null @@ -1,16 +0,0 @@ -# LLM Warmup — ponyiser (User) - -## What is ponyiser? -See README.adoc for overview. - -## Key Commands -- `just setup` — set up development environment -- `just build` — build the project -- `just test` — run tests -- `just doctor` — diagnose issues -- `just heal` — attempt auto-repair - -## Quick Context -- License: MPL-2.0 -- Part of hyperpolymath ecosystem -- See EXPLAINME.adoc for architecture