From 6126c7f7f9f86359cd2f3afb703e892b97baaa32 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 23 Aug 2026 20:04:38 +0100 Subject: [PATCH 1/2] chore: global textual eradication of Nix and ReScript --- .github/CONTRIBUTING.md | 6 +++--- .github/copilot-instructions.md | 2 +- .github/dependabot.yml | 4 ++-- .machine_readable/ai/PLACEHOLDERS.adoc | 6 +++--- .../contractiles/lust/Intentfile.a2ml | 2 +- .../policies/MAINTENANCE-CHECKLIST.a2ml | 2 +- CONTRIBUTING.md | 2 +- docs/RSR_OUTLINE.adoc | 8 ++++---- docs/STATE-VISUALIZER.adoc | 4 ++-- docs/developer/ABI-FFI-README.adoc | 4 ++-- docs/governance/MAINTENANCE-CHECKLIST.a2ml | 2 +- docs/practice/AI-CONVENTIONS.adoc | 2 +- examples/web-project-deno.json | 16 ++++++++-------- 13 files changed, 30 insertions(+), 30 deletions(-) diff --git a/.github/CONTRIBUTING.md b/.github/CONTRIBUTING.md index 62d32e5..017c8e9 100644 --- a/.github/CONTRIBUTING.md +++ b/.github/CONTRIBUTING.md @@ -2,8 +2,8 @@ git clone https://github.com/hyperpolymath/ephapaxiser.git cd ephapaxiser -# Using Nix (recommended for reproducibility) -nix develop +# Using Guix (recommended for reproducibility) +guix develop # Or using toolbox/distrobox toolbox create ephapaxiser-dev @@ -45,7 +45,7 @@ ephapaxiser/ ├── MAINTAINERS.md ├── README.adoc ├── SECURITY.md -├── flake.nix # Nix flake — fallback (Perimeter 1) +├── flake.guix # Guix flake — fallback (Perimeter 1) ├── guix.scm # Guix package — primary (Perimeter 1) └── Justfile # Task runner (Perimeter 1) ``` diff --git a/.github/copilot-instructions.md b/.github/copilot-instructions.md index 6e2bea9..678e4a4 100644 --- a/.github/copilot-instructions.md +++ b/.github/copilot-instructions.md @@ -33,7 +33,7 @@ ## Banned Languages -- No TypeScript (use ReScript) +- No TypeScript (use AffineScript) - No Node.js / npm / bun (use Deno) - No Go (use Rust) - No Python (use Julia or Rust) diff --git a/.github/dependabot.yml b/.github/dependabot.yml index d5cd4e9..045cb8f 100644 --- a/.github/dependabot.yml +++ b/.github/dependabot.yml @@ -41,8 +41,8 @@ updates: schedule: interval: "weekly" - # Nix flakes - - package-ecosystem: "nix" + # Guix flakes + - package-ecosystem: "guix" directory: "/" schedule: interval: "weekly" diff --git a/.machine_readable/ai/PLACEHOLDERS.adoc b/.machine_readable/ai/PLACEHOLDERS.adoc index 187e1e9..f0c1144 100644 --- a/.machine_readable/ai/PLACEHOLDERS.adoc +++ b/.machine_readable/ai/PLACEHOLDERS.adoc @@ -48,8 +48,8 @@ sed -i "s/{{CURRENT_DATE}}/$(date +%Y-%m-%d)/g" $(grep -rl '{{CURRENT_DATE}}' .) | Placeholder | Description | Example | Files | |---|---|---|---| -| `{{PROJECT_NAME}}` | Human-readable project name | `My Project` | SECURITY.md, CODE_OF_CONDUCT.md, TOPOLOGY.md, STATE.a2ml, Justfile, GOVERNANCE.md, MAINTAINERS.md, flake.nix, devcontainer.json | -| `{{PROJECT_DESCRIPTION}}` | One-line description | `A tool for X` | flake.nix | +| `{{PROJECT_NAME}}` | Human-readable project name | `My Project` | SECURITY.md, CODE_OF_CONDUCT.md, TOPOLOGY.md, STATE.a2ml, Justfile, GOVERNANCE.md, MAINTAINERS.md, flake.guix, devcontainer.json | +| `{{PROJECT_DESCRIPTION}}` | One-line description | `A tool for X` | flake.guix | | `{{PROJECT}}` | Uppercase identifier (for Idris2 modules, C macros) | `MY_PROJECT` | ABI-FFI-README.md, src/interface/abi/*.idr, src/interface/ffi/*.zig | | `{{project}}` | Lowercase identifier (for C symbols, filenames) | `my_project` | ABI-FFI-README.md, src/interface/ffi/*.zig | | `ephapaxiser` | Repository name (slug) | `my-project` | CONTRIBUTING.md, SECURITY.md, CODE_OF_CONDUCT.md, cliff.toml | @@ -133,7 +133,7 @@ After replacing all placeholders, verify none remain: ```bash grep -rn '{{' . --include='*.md' --include='*.adoc' --include='*.a2ml' \ --include='*.scm' --include='*.idr' --include='*.zig' --include='*.res' \ - --include='Justfile' --include='*.nix' --include='*.toml' --include='*.yml' \ + --include='Justfile' --include='*.guix' --include='*.toml' --include='*.yml' \ --include='*.yaml' --include='*.hs' --include='*.ncl' --include='*.txt' \ --include='*.json' --include='Containerfile' --include='dep5' \ | grep -v 'PLACEHOLDERS.md' | grep -v 'node_modules' diff --git a/.machine_readable/contractiles/lust/Intentfile.a2ml b/.machine_readable/contractiles/lust/Intentfile.a2ml index 212d209..16e1ea3 100644 --- a/.machine_readable/contractiles/lust/Intentfile.a2ml +++ b/.machine_readable/contractiles/lust/Intentfile.a2ml @@ -16,7 +16,7 @@ design philosophy — not current state, but target state. ### reproducible-builds - description: Builds should be bit-for-bit reproducible -- target: Guix + Nix + Containerfile +- target: Guix + Guix + Containerfile - status: aspiration ### zero-dangerous-patterns diff --git a/.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml b/.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml index eaee720..698f4d0 100644 --- a/.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml +++ b/.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml @@ -67,7 +67,7 @@ compliance-seams-check = true exception-register-required = true exception-bounded-scope-required = true policy-drift-contamination-check = true -example-drift-risk = "single TypeScript exception causing broad ReScript->TypeScript migration" +example-drift-risk = "single TypeScript exception causing broad AffineScript->TypeScript migration" compliance-tooling = "panic-attack" effects-tooling = "ecological checking with sustainabot guidance" diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 80ecdac..90e87dc 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -15,7 +15,7 @@ We welcome contributions in many forms: ## 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. +2. **Environment:** Use `guix develop` or `direnv allow` to set up your tools. 3. **Task Runner:** Use `just` to see available commands (`just --list`). ## Development Workflow diff --git a/docs/RSR_OUTLINE.adoc b/docs/RSR_OUTLINE.adoc index 8faf3bb..83e1c15 100644 --- a/docs/RSR_OUTLINE.adoc +++ b/docs/RSR_OUTLINE.adoc @@ -204,8 +204,8 @@ project/ === Language Tiers -* **Tier 1** (Gold): Rust, Elixir, Zig, Ada, Haskell, ReScript, Gleam -* **Tier 2** (Silver): Nickel, Guile Scheme, Nix, Idris2, OCaml +* **Tier 1** (Gold): Rust, Elixir, Zig, Ada, Haskell, AffineScript, Gleam +* **Tier 2** (Silver): Nickel, Guile Scheme, Guix, Idris2, OCaml * **Infrastructure**: Guix channels, derivations, Julia batch scripts === Required Files @@ -219,12 +219,12 @@ project/ * `.well-known/security.txt` * `.well-known/ai.txt` * `.well-known/humans.txt` -* `guix.scm` OR `flake.nix` +* `guix.scm` OR `flake.guix` === Prohibited * Python outside `salt/` directory -* TypeScript/JavaScript (use ReScript) +* TypeScript/JavaScript (use AffineScript) * CUE (use Guile/Nickel) * `Dockerfile` (use `Containerfile`) * npm, Bun, pnpm, yarn (use Deno) diff --git a/docs/STATE-VISUALIZER.adoc b/docs/STATE-VISUALIZER.adoc index 4be8d44..7746b12 100644 --- a/docs/STATE-VISUALIZER.adoc +++ b/docs/STATE-VISUALIZER.adoc @@ -46,7 +46,7 @@ ┌─────────────────────────────────────────┐ │ PLATFORM INTEGRATION │ │ ┌───────────┐ ┌───────────┐ ┌───────┐│ - │ │ GitHub │ │ GitLab │ │ Nix / ││ + │ │ GitHub │ │ GitLab │ │ Guix / ││ │ │ Workflows │ │ CI/CD │ │ Guix ││ │ └───────────┘ └───────────┘ └───────┘│ └─────────────────────────────────────────┘ @@ -88,7 +88,7 @@ CONTAINER ECOSYSTEM (Phase 2) REPO INFRASTRUCTURE .machine_readable/ ██████████ 100% STATE/META/ECOSYSTEM active Governance & License ██████████ 100% MPL-2.0 & Ethical use verified - Development Shells (Nix/Guix) ██████████ 100% Reproducible env stable + Development Shells (Guix/Guix) ██████████ 100% Reproducible env stable ───────────────────────────────────────────────────────────────────────────── OVERALL: ██████████ 100% RSR Template Stable & Certified diff --git a/docs/developer/ABI-FFI-README.adoc b/docs/developer/ABI-FFI-README.adoc index fe01f12..dd5db7a 100644 --- a/docs/developer/ABI-FFI-README.adoc +++ b/docs/developer/ABI-FFI-README.adoc @@ -44,7 +44,7 @@ This library follows the **Hyperpolymath RSR Standard** for ABI and FFI design: ▼ ┌─────────────────────────────────────────────┐ │ Any Language via C ABI │ -│ - Rust, ReScript, Julia, Python, etc. │ +│ - Rust, AffineScript, Julia, Python, etc. │ └─────────────────────────────────────────────┘ ``` @@ -76,7 +76,7 @@ This library follows the **Hyperpolymath RSR Standard** for ABI and FFI design: │ └── bindings/ # Language-specific wrappers (optional) ├── rust/ - ├── rescript/ + ├── affinescript/ └── julia/ ``` diff --git a/docs/governance/MAINTENANCE-CHECKLIST.a2ml b/docs/governance/MAINTENANCE-CHECKLIST.a2ml index eaee720..698f4d0 100644 --- a/docs/governance/MAINTENANCE-CHECKLIST.a2ml +++ b/docs/governance/MAINTENANCE-CHECKLIST.a2ml @@ -67,7 +67,7 @@ compliance-seams-check = true exception-register-required = true exception-bounded-scope-required = true policy-drift-contamination-check = true -example-drift-risk = "single TypeScript exception causing broad ReScript->TypeScript migration" +example-drift-risk = "single TypeScript exception causing broad AffineScript->TypeScript migration" compliance-tooling = "panic-attack" effects-tooling = "ecological checking with sustainabot guidance" diff --git a/docs/practice/AI-CONVENTIONS.adoc b/docs/practice/AI-CONVENTIONS.adoc index 58e132b..6a3636b 100644 --- a/docs/practice/AI-CONVENTIONS.adoc +++ b/docs/practice/AI-CONVENTIONS.adoc @@ -53,7 +53,7 @@ MAINTENANCE-CHECKLIST.a2ml, or SOFTWARE-DEVELOPMENT-APPROACH.a2ml in the reposit | Banned | Use Instead | |---------------------|--------------------| -| TypeScript | ReScript | +| TypeScript | AffineScript | | Node.js / npm / bun | Deno | | Go | Rust | | Python | Julia / Rust | diff --git a/examples/web-project-deno.json b/examples/web-project-deno.json index 5ddd3bd..ee775a4 100644 --- a/examples/web-project-deno.json +++ b/examples/web-project-deno.json @@ -1,17 +1,17 @@ { - "// NOTE": "Example deno.json for ReScript web projects", + "// NOTE": "Example deno.json for AffineScript web projects", "tasks": { - "build": "deno run -A npm:rescript", - "clean": "deno run -A npm:rescript clean", - "watch": "deno run -A npm:rescript -w", + "build": "deno run -A npm:affinescript", + "clean": "deno run -A npm:affinescript clean", + "watch": "deno run -A npm:affinescript -w", "serve": "deno run -A jsr:@std/http/file-server .", "test": "deno test --allow-all" }, "imports": { - "rescript": "^12.0.0", - "@rescript/core": "npm:@rescript/core@^1.6.0", - "safe-dom/": "https://raw.githubusercontent.com/hyperpolymath/rescript-dom-mounter/main/src/", - "proven/": "../proven/bindings/rescript/src/" + "affinescript": "^12.0.0", + "@affinescript/core": "npm:@affinescript/core@^1.6.0", + "safe-dom/": "https://raw.githubusercontent.com/hyperpolymath/affinescript-dom-mounter/main/src/", + "proven/": "../proven/bindings/affinescript/src/" }, "compilerOptions": { "allowJs": true, From c8981c7f59a35eb9da7c4e681bd9505bfa8637df Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 24 Aug 2026 08:11:08 +0100 Subject: [PATCH 2/2] refactor: migrate repository documentation from Markdown to AsciiDoc --- CODE_OF_CONDUCT.adoc | 24 +++++ CODE_OF_CONDUCT.md | 27 ------ CONTRIBUTING.adoc | 71 ++++++++++++++ CONTRIBUTING.md | 66 ------------- README.adoc | 158 +++++++++++++++++++++++++++++++ README.md | 178 ----------------------------------- SECURITY.md => SECURITY.adoc | 21 +++-- TEST-NEEDS.adoc | 34 +++++++ TEST-NEEDS.md | 31 ------ TOPOLOGY.md => TOPOLOGY.adoc | 40 ++++---- llm-warmup-dev.adoc | 19 ++++ llm-warmup-dev.md | 16 ---- llm-warmup-user.adoc | 19 ++++ llm-warmup-user.md | 16 ---- 14 files changed, 358 insertions(+), 362 deletions(-) create mode 100644 CODE_OF_CONDUCT.adoc delete mode 100644 CODE_OF_CONDUCT.md create mode 100644 CONTRIBUTING.adoc delete mode 100644 CONTRIBUTING.md create mode 100644 README.adoc delete mode 100644 README.md rename SECURITY.md => SECURITY.adoc (58%) create mode 100644 TEST-NEEDS.adoc delete mode 100644 TEST-NEEDS.md rename TOPOLOGY.md => TOPOLOGY.adoc (90%) create mode 100644 llm-warmup-dev.adoc delete mode 100644 llm-warmup-dev.md create mode 100644 llm-warmup-user.adoc delete mode 100644 llm-warmup-user.md 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..dd089ae --- /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 `+guix 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 90e87dc..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 `guix 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/README.adoc b/README.adoc new file mode 100644 index 0000000..505b783 --- /dev/null +++ b/README.adoc @@ -0,0 +1,158 @@ +== What Is This? + +Ephapaxiser analyses code for resource handles, inserts +https://github.com/hyperpolymath[Ephapax] linear type wrappers around +them, and enforces *exactly-once usage* at compile time. The result: +resource leaks, double-frees, and use-after-free bugs become +_impossible_ in wrapped code. + +Ephapax (from Greek _ἐφάπαξ_ — "`once for all`") is hyperpolymath’s +linear type language where every value must be used exactly once. +Ephapaxiser brings those guarantees to existing Rust, C, and Zig +codebases without requiring the developer to learn Ephapax itself. + +== How It Works + +Describe your resources in an `+ephapaxiser.toml+` manifest. Ephapaxiser +then: + +[arabic] +. *Analyses* your source code for resource acquisition and release +patterns (file handles, sockets, database connections, GPU buffers, +crypto keys) +. *Generates* Ephapax linear type wrappers that structurally enforce +single-use semantics on each resource +. *Proves* linearity via the Idris2 ABI layer — dependent types +guarantee that every resource is consumed exactly once +. *Bridges* proofs into executable code via the Zig FFI — zero runtime +overhead, proofs are erased at compile time +. *Emits* target-language wrapper code that the developer can drop in +place + +If a resource is used after consumption, leaked, or double-freed, you +get a *compile-time error* — not a runtime crash. + +== Key Value + +* *Resource leaks become compile errors* — files always closed, keys +always zeroised, connections always released +* *Use-after-free impossible* — linear types structurally prevent it +* *Double-free impossible* — consumption proof means the resource cannot +be freed twice +* *Crypto key safety* — keys used exactly once then destroyed (perfect +forward secrecy enforcement) +* *GPU buffer lifecycle* — allocate, use, release: compile-time +guarantee the buffer is not accessed after release +* *Database connection pooling* — connections checked out exactly once, +always returned +* *Session token safety* — tokens consumed on use, preventing replay +* *Gradual adoption* — wrap one resource type at a time in existing code + +== Architecture + +Ephapaxiser follows the hyperpolymath +https://github.com/hyperpolymath/iseriser[-iser pattern]: + +.... +ephapaxiser.toml manifest + │ + ▼ + Resource Analysis (Rust CLI) + ── identify acquire/release patterns + │ + ▼ + Idris2 ABI (src/interface/abi/) + ── LinearResource, UsageCount, ConsumeProof + ── dependent types PROVE linearity invariants + │ + ▼ + Zig FFI (src/interface/ffi/) + ── C-ABI bridge, zero overhead + │ + ▼ + Ephapax Codegen (src/codegen/) + ── emit target-language wrappers + ── Rust / C / Zig output +.... + +=== Idris2 ABI Layer + +The Idris2 ABI layer (`+src/interface/abi/+`) is the formal +specification: + +* `+Types.idr+` — `+LinearResource+`, `+UsageCount+`, +`+ResourceLifecycle+`, `+ConsumeProof+` — types that express "`this +resource is used exactly once`" +* `+Layout.idr+` — memory layout for resource tracking structs, with +padding and alignment proofs +* `+Foreign.idr+` — FFI declarations for resource analysis and linearity +enforcement operations + +=== Idris2 Wins Rule + +____ +[!IMPORTANT] *When Idris2 proofs conflict with Ephapax linear types, +Idris2 always wins.* + +This is a standing project rule across all hyperpolymath repositories. +The formally verified Idris2 proofs are the source of truth. If an +Ephapax wrapper would violate a proven Idris2 invariant, the wrapper +must be adjusted — never the proof. +____ + +=== Zig FFI Layer + +The Zig FFI layer (`+src/interface/ffi/+`) implements the C-ABI bridge +declared by the Idris2 ABI. It provides: + +* Resource handle lifecycle (init/free with linearity tracking) +* Resource consumption operations (use-once semantics enforced) +* Thread-local error reporting +* Cross-platform compilation (Linux, macOS, Windows, WASM) + +== Use Cases + +* *File handle management* — ensure every opened file is closed exactly +once +* *Database connections* — prevent connection leaks in pooled +environments +* *GPU buffer lifecycle* — allocate, compute, release — no dangling +buffers +* *Session tokens* — single-use tokens that cannot be replayed +* *Crypto key material* — keys consumed on use, then securely zeroised +* *Network sockets* — no forgotten open connections + +== Status + +*Codebase in progress.* Architecture defined, Rust CLI scaffolded, +Idris2 ABI and Zig FFI stubs in place. Resource analysis and Ephapax +codegen are the active development frontier. + +See link:ROADMAP.adoc[ROADMAP] for the full phase plan. + +== Quick Start + +[source,bash] +---- +# Initialise a manifest in your project +ephapaxiser init --path . + +# Edit ephapaxiser.toml to describe your resources +# Then generate wrappers +ephapaxiser generate --manifest ephapaxiser.toml --output generated/ + +# Validate your manifest +ephapaxiser validate --manifest ephapaxiser.toml +---- + +== Build + +[source,bash] +---- +cargo build --release +cargo test +---- + +== License + +SPDX-License-Identifier: CC-BY-SA-4.0 diff --git a/README.md b/README.md deleted file mode 100644 index 94caf19..0000000 --- a/README.md +++ /dev/null @@ -1,178 +0,0 @@ - - -# What Is This? - -Ephapaxiser analyses code for resource handles, inserts -[Ephapax](https://github.com/hyperpolymath) linear type wrappers around -them, and enforces **exactly-once usage** at compile time. The result: -resource leaks, double-frees, and use-after-free bugs become -*impossible* in wrapped code. - -Ephapax (from Greek *ἐφάπαξ* — "once for all") is hyperpolymath’s linear -type language where every value must be used exactly once. Ephapaxiser -brings those guarantees to existing Rust, C, and Zig codebases without -requiring the developer to learn Ephapax itself. - -# How It Works - -Describe your resources in an `ephapaxiser.toml` manifest. Ephapaxiser -then: - -1. **Analyses** your source code for resource acquisition and release - patterns (file handles, sockets, database connections, GPU buffers, - crypto keys) - -2. **Generates** Ephapax linear type wrappers that structurally enforce - single-use semantics on each resource - -3. **Proves** linearity via the Idris2 ABI layer — dependent types - guarantee that every resource is consumed exactly once - -4. **Bridges** proofs into executable code via the Zig FFI — zero - runtime overhead, proofs are erased at compile time - -5. **Emits** target-language wrapper code that the developer can drop - in place - -If a resource is used after consumption, leaked, or double-freed, you -get a **compile-time error** — not a runtime crash. - -# Key Value - -- **Resource leaks become compile errors** — files always closed, keys - always zeroised, connections always released - -- **Use-after-free impossible** — linear types structurally prevent it - -- **Double-free impossible** — consumption proof means the resource - cannot be freed twice - -- **Crypto key safety** — keys used exactly once then destroyed (perfect - forward secrecy enforcement) - -- **GPU buffer lifecycle** — allocate, use, release: compile-time - guarantee the buffer is not accessed after release - -- **Database connection pooling** — connections checked out exactly - once, always returned - -- **Session token safety** — tokens consumed on use, preventing replay - -- **Gradual adoption** — wrap one resource type at a time in existing - code - -# Architecture - -Ephapaxiser follows the hyperpolymath [-iser -pattern](https://github.com/hyperpolymath/iseriser): - - ephapaxiser.toml manifest - │ - ▼ - Resource Analysis (Rust CLI) - ── identify acquire/release patterns - │ - ▼ - Idris2 ABI (src/interface/abi/) - ── LinearResource, UsageCount, ConsumeProof - ── dependent types PROVE linearity invariants - │ - ▼ - Zig FFI (src/interface/ffi/) - ── C-ABI bridge, zero overhead - │ - ▼ - Ephapax Codegen (src/codegen/) - ── emit target-language wrappers - ── Rust / C / Zig output - -## Idris2 ABI Layer - -The Idris2 ABI layer (`src/interface/abi/`) is the formal specification: - -- `Types.idr` — `LinearResource`, `UsageCount`, `ResourceLifecycle`, - `ConsumeProof` — types that express "this resource is used exactly - once" - -- `Layout.idr` — memory layout for resource tracking structs, with - padding and alignment proofs - -- `Foreign.idr` — FFI declarations for resource analysis and linearity - enforcement operations - -## Idris2 Wins Rule - -> [!IMPORTANT] -> **When Idris2 proofs conflict with Ephapax linear types, Idris2 always -> wins.** -> -> This is a standing project rule across all hyperpolymath repositories. -> The formally verified Idris2 proofs are the source of truth. If an -> Ephapax wrapper would violate a proven Idris2 invariant, the wrapper -> must be adjusted — never the proof. - -## Zig FFI Layer - -The Zig FFI layer (`src/interface/ffi/`) implements the C-ABI bridge -declared by the Idris2 ABI. It provides: - -- Resource handle lifecycle (init/free with linearity tracking) - -- Resource consumption operations (use-once semantics enforced) - -- Thread-local error reporting - -- Cross-platform compilation (Linux, macOS, Windows, WASM) - -# Use Cases - -- **File handle management** — ensure every opened file is closed - exactly once - -- **Database connections** — prevent connection leaks in pooled - environments - -- **GPU buffer lifecycle** — allocate, compute, release — no dangling - buffers - -- **Session tokens** — single-use tokens that cannot be replayed - -- **Crypto key material** — keys consumed on use, then securely zeroised - -- **Network sockets** — no forgotten open connections - -# Status - -**Codebase in progress.** Architecture defined, Rust CLI scaffolded, -Idris2 ABI and Zig FFI stubs in place. Resource analysis and Ephapax -codegen are the active development frontier. - -See [ROADMAP](ROADMAP.adoc) for the full phase plan. - -# Quick Start - -```bash -# Initialise a manifest in your project -ephapaxiser init --path . - -# Edit ephapaxiser.toml to describe your resources -# Then generate wrappers -ephapaxiser generate --manifest ephapaxiser.toml --output generated/ - -# Validate your manifest -ephapaxiser validate --manifest ephapaxiser.toml -``` - -# Build - -```bash -cargo build --release -cargo test -``` - -# License - -SPDX-License-Identifier: CC-BY-SA-4.0 diff --git a/SECURITY.md b/SECURITY.adoc similarity index 58% rename from SECURITY.md rename to SECURITY.adoc index 49065d4..42dce28 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 ephapaxiser CLI tool and its generated artifacts. diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc new file mode 100644 index 0000000..3875686 --- /dev/null +++ b/TEST-NEEDS.adoc @@ -0,0 +1,34 @@ +== TEST-NEEDS.md — ephapaxiser + +=== CRG Grade: C — ACHIEVED 2026-04-04 + +=== Current Test State + +[cols=",,",options="header",] +|=== +|Category |Count |Notes +|Test directories |2 |Location(s): /tests, /verification/tests +|CI workflows |22 |Running tests on GitHub Actions +|Unit tests |Built-in |Rust/cargo test framework +|Integration tests |Configured |Via integration/ directory +|=== + +=== What’s Covered + +* [x] Rust unit test suite (cargo test) +* [x] Documentation tests +* [x] Example programs with tests + +=== Still Missing (for CRG B+) + +* [ ] Code coverage reports (codecov integration) +* [ ] Detailed test documentation in CONTRIBUTING.md +* [ ] Integration tests beyond unit tests +* [ ] Performance benchmarking suite + +=== Run Tests + +[source,bash] +---- +cargo test +---- diff --git a/TEST-NEEDS.md b/TEST-NEEDS.md deleted file mode 100644 index 36d4670..0000000 --- a/TEST-NEEDS.md +++ /dev/null @@ -1,31 +0,0 @@ -# TEST-NEEDS.md — ephapaxiser - -## CRG Grade: C — ACHIEVED 2026-04-04 - -## Current Test State - -| Category | Count | Notes | -|----------|-------|-------| -| Test directories | 2 | Location(s): /tests, /verification/tests | -| CI workflows | 22 | Running tests on GitHub Actions | -| Unit tests | Built-in | Rust/cargo test framework | -| Integration tests | Configured | Via integration/ directory | - -## What's Covered - -- [x] Rust unit test suite (cargo test) -- [x] Documentation tests -- [x] Example programs with tests - -## Still Missing (for CRG B+) - -- [ ] Code coverage reports (codecov integration) -- [ ] Detailed test documentation in CONTRIBUTING.md -- [ ] Integration tests beyond unit tests -- [ ] Performance benchmarking suite - -## Run Tests - -```bash -cargo test -``` diff --git a/TOPOLOGY.md b/TOPOLOGY.adoc similarity index 90% rename from TOPOLOGY.md rename to TOPOLOGY.adoc index 386fde0..0aae4a7 100644 --- a/TOPOLOGY.md +++ b/TOPOLOGY.adoc @@ -1,12 +1,10 @@ - - -# TOPOLOGY — ephapaxiser +== TOPOLOGY — ephapaxiser Repository structure and module relationships for ephapaxiser. -## Directory Map +=== Directory Map -``` +.... ephapaxiser/ ├── 0-AI-MANIFEST.a2ml # AI agent entry point (read first) ├── Cargo.toml # Rust package definition @@ -97,11 +95,11 @@ ephapaxiser/ ├── .hypatia/ # Hypatia scanner rules ├── .claude/ # Claude Code project instructions └── .well-known/ # Well-known URIs -``` +.... -## Data Flow +=== Data Flow -``` +.... ephapaxiser.toml │ ┌────────▼────────┐ @@ -138,18 +136,22 @@ ephapaxiser/ ▼ wrapped source code (compile-time safe) -``` +.... -## Key Invariants +=== Key Invariants -1. **Idris2 wins**: When Idris2 proofs conflict with Ephapax linear types, - the proofs are authoritative. Adjust wrappers, never proofs. -2. **Single-use**: Every wrapped resource must be consumed exactly once. - This is enforced structurally, not by convention. -3. **Zero runtime overhead**: All linearity proofs are erased at compile time. -4. **Machine-readable in `.machine_readable/` only**: No state files in root. +[arabic] +. *Idris2 wins*: When Idris2 proofs conflict with Ephapax linear types, +the proofs are authoritative. Adjust wrappers, never proofs. +. *Single-use*: Every wrapped resource must be consumed exactly once. +This is enforced structurally, not by convention. +. *Zero runtime overhead*: All linearity proofs are erased at compile +time. +. *Machine-readable in `+.machine_readable/+` only*: No state files in +root. -## Ecosystem Position +=== Ecosystem Position -Part of the [hyperpolymath -iser family](https://github.com/hyperpolymath/iseriser). -Siblings include typedqliser, chapeliser, verisimiser, and 26+ others. +Part of the https://github.com/hyperpolymath/iseriser[hyperpolymath +-iser family]. Siblings include typedqliser, chapeliser, verisimiser, +and 26+ others. diff --git a/llm-warmup-dev.adoc b/llm-warmup-dev.adoc new file mode 100644 index 0000000..2df4ef8 --- /dev/null +++ b/llm-warmup-dev.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — ephapaxiser (Developer) + +=== What is ephapaxiser? + +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 b7a71f7..0000000 --- a/llm-warmup-dev.md +++ /dev/null @@ -1,16 +0,0 @@ -# LLM Warmup — ephapaxiser (Developer) - -## What is ephapaxiser? -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..9bad547 --- /dev/null +++ b/llm-warmup-user.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — ephapaxiser (User) + +=== What is ephapaxiser? + +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 057f1c4..0000000 --- a/llm-warmup-user.md +++ /dev/null @@ -1,16 +0,0 @@ -# LLM Warmup — ephapaxiser (User) - -## What is ephapaxiser? -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