|
| 1 | +<!-- |
| 2 | +SPDX-License-Identifier: CC-BY-SA-4.0 |
| 3 | +SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 4 | +--> |
| 5 | + |
| 6 | +[](https://github.com/sponsors/hyperpolymath) |
| 7 | + |
| 8 | +# What Is Affinescriptiser? |
| 9 | + |
| 10 | +Affinescriptiser takes existing code written in Rust, C, or Zig and |
| 11 | +wraps it with |
| 12 | +[AffineScript](https://github.com/hyperpolymath/affinescript)’s type |
| 13 | +system — combining **affine types** (resources used at most once) with |
| 14 | +**dependent types** (compile-time value constraints) — then compiles the |
| 15 | +result to **WebAssembly**. |
| 16 | + |
| 17 | +The outcome: resources such as file descriptors, sockets, GPU buffers, |
| 18 | +and heap allocations become **provably** safe. They cannot be leaked, |
| 19 | +double-freed, or used after release. The wrapped code ships as a `.wasm` |
| 20 | +binary with zero garbage collector and zero runtime overhead from the |
| 21 | +type proofs. |
| 22 | + |
| 23 | +Affinescriptiser is part of the [-iser |
| 24 | +family](https://github.com/hyperpolymath/iseriser), a collection of |
| 25 | +tools that wrap existing code in a target language’s capabilities |
| 26 | +without requiring users to learn that language. |
| 27 | + |
| 28 | +# How It Works |
| 29 | + |
| 30 | +You describe your code in an `affinescriptiser.toml` manifest, point at |
| 31 | +your source files, and declare which resources need affine tracking. |
| 32 | + |
| 33 | +```toml |
| 34 | +# affinescriptiser.toml — example manifest |
| 35 | +[workload] |
| 36 | +name = "secure-file-processor" |
| 37 | +entry = "src/lib.rs::process_file" |
| 38 | +strategy = "affine-wrap" |
| 39 | + |
| 40 | +[data] |
| 41 | +input-type = "FileHandle" |
| 42 | +output-type = "ProcessedResult" |
| 43 | + |
| 44 | +[options] |
| 45 | +flags = ["track-file-descriptors", "track-allocations", "wasm-size-opt"] |
| 46 | +``` |
| 47 | + |
| 48 | +Affinescriptiser then: |
| 49 | + |
| 50 | +1. **Analyses** your function signatures and identifies resource |
| 51 | + handles (file descriptors, heap allocations, locks, GPU buffers) |
| 52 | + |
| 53 | +2. **Generates** AffineScript type annotations that enforce |
| 54 | + at-most-once usage for each tracked resource |
| 55 | + |
| 56 | +3. **Proves** via Idris2 that affine invariants hold across the FFI |
| 57 | + boundary |
| 58 | + |
| 59 | +4. **Compiles** the wrapped code to WebAssembly with size and |
| 60 | + performance optimisation |
| 61 | + |
| 62 | +# Architecture |
| 63 | + |
| 64 | + affinescriptiser pipeline |
| 65 | + ┌──────────────────────────────────────────────────────────────────────────┐ |
| 66 | + │ │ |
| 67 | + │ ┌─────────────────┐ ┌───────────────────┐ ┌────────────────┐ │ |
| 68 | + │ │ affinescriptiser │ │ Source Analysis │ │ Idris2 ABI │ │ |
| 69 | + │ │ .toml │────▶│ (Rust CLI) │────▶│ Proofs │ │ |
| 70 | + │ │ │ │ │ │ │ │ |
| 71 | + │ │ - entry point │ │ - parse signatures│ │ - ResourceKind│ │ |
| 72 | + │ │ - resource list │ │ - find handles │ │ - Linearity │ │ |
| 73 | + │ │ - WASM flags │ │ - map ownership │ │ - Ownership │ │ |
| 74 | + │ └─────────────────┘ └───────────────────┘ └───────┬────────┘ │ |
| 75 | + │ │ │ |
| 76 | + │ ▼ │ |
| 77 | + │ ┌─────────────────┐ ┌───────────────────┐ ┌────────────────┐ │ |
| 78 | + │ │ .wasm output │◀────│ AffineScript │◀────│ Zig FFI │ │ |
| 79 | + │ │ │ │ Codegen │ │ Bridge │ │ |
| 80 | + │ │ - zero GC │ │ │ │ │ │ |
| 81 | + │ │ - size-optimised│ │ - affine wrappers │ │ - C headers │ │ |
| 82 | + │ │ - portable │ │ - effect handlers │ │ - zero-cost │ │ |
| 83 | + │ └─────────────────┘ └───────────────────┘ └────────────────┘ │ |
| 84 | + │ │ |
| 85 | + └──────────────────────────────────────────────────────────────────────────┘ |
| 86 | + |
| 87 | +## Layer Responsibilities |
| 88 | + |
| 89 | +| Layer | Role | |
| 90 | +|----|----| |
| 91 | +| **Manifest** (`affinescriptiser.toml`) | User declares what code to wrap and which resources to track. | |
| 92 | +| **Source Analysis** (Rust, `src/manifest/`, `src/codegen/`) | Parses input source files, identifies resource handles and ownership patterns. | |
| 93 | +| **Idris2 ABI** (`src/interface/abi/`) | Formal proofs that affine invariants (at-most-once usage, no leaks) hold. Defines `ResourceKind`, `Linearity`, `Ownership`, and WASM memory layout. | |
| 94 | +| **Zig FFI** (`src/interface/ffi/`) | C-ABI compatible bridge between the proven ABI and the generated code. Zero runtime overhead, cross-compilation built in. | |
| 95 | +| **AffineScript Codegen** (`src/codegen/`) | Generates AffineScript wrapper code with ownership annotations and algebraic effect handlers. Compiles to WASM. | |
| 96 | +| **WASM Output** | Final `.wasm` binary. No garbage collector, no runtime, minimal size. | |
| 97 | + |
| 98 | +# Key Value |
| 99 | + |
| 100 | +**Automatic resource safety** — files, sockets, GPU buffers, and heap |
| 101 | +allocations cannot be leaked or double-freed. The type system proves |
| 102 | +this at compile time, not at runtime. |
| 103 | + |
| 104 | +**WASM deployment** — the output is a portable WebAssembly binary that |
| 105 | +runs in browsers, edge workers, IoT devices, or any WASM runtime. No GC |
| 106 | +means predictable latency and tiny binary size. |
| 107 | + |
| 108 | +**Zero target-language exposure** — users never write AffineScript |
| 109 | +directly. They describe their intent in TOML and let affinescriptiser |
| 110 | +handle the wrapping, proving, and compilation. |
| 111 | + |
| 112 | +# Use Cases |
| 113 | + |
| 114 | +- **Browser sandboxed computation** — run resource-safe code in the |
| 115 | + browser via WASM without worrying about memory leaks in long-running |
| 116 | + tabs |
| 117 | + |
| 118 | +- **Edge computing** — deploy provably-safe WASM modules to Cloudflare |
| 119 | + Workers, Fastly Compute, or Deno Deploy with guaranteed resource |
| 120 | + bounds |
| 121 | + |
| 122 | +- **IoT firmware** — compile to WASM for microcontrollers with formal |
| 123 | + proof that bounded memory is respected |
| 124 | + |
| 125 | +- **GPU buffer management** — wrap CUDA/Vulkan buffer allocations with |
| 126 | + affine types to prevent double-free and use-after-free in compute |
| 127 | + shaders |
| 128 | + |
| 129 | +- **Secure file processing** — process sensitive files with compile-time |
| 130 | + proof that file handles are closed exactly once |
| 131 | + |
| 132 | +# CLI Commands |
| 133 | + |
| 134 | +```bash |
| 135 | +# Initialise a new manifest in the current directory |
| 136 | +affinescriptiser init |
| 137 | + |
| 138 | +# Validate your manifest |
| 139 | +affinescriptiser validate -m affinescriptiser.toml |
| 140 | + |
| 141 | +# Generate AffineScript wrappers, Zig FFI bridge, and C headers |
| 142 | +affinescriptiser generate -m affinescriptiser.toml -o generated/affinescriptiser |
| 143 | + |
| 144 | +# Build the generated artifacts |
| 145 | +affinescriptiser build -m affinescriptiser.toml --release |
| 146 | + |
| 147 | +# Run the workload |
| 148 | +affinescriptiser run -m affinescriptiser.toml -- --input data.bin |
| 149 | + |
| 150 | +# Show manifest information |
| 151 | +affinescriptiser info -m affinescriptiser.toml |
| 152 | +``` |
| 153 | + |
| 154 | +# Building from Source |
| 155 | + |
| 156 | +```bash |
| 157 | +# Prerequisites: Rust (nightly), Idris2, Zig |
| 158 | +cargo build --release |
| 159 | + |
| 160 | +# Run tests |
| 161 | +cargo test |
| 162 | + |
| 163 | +# Full quality check (format, lint, test) |
| 164 | +just quality |
| 165 | +``` |
| 166 | + |
| 167 | +# Status |
| 168 | + |
| 169 | +**Pre-alpha / Scaffold.** The architecture is defined, the CLI is |
| 170 | +functional (init, validate, info), and the RSR template with full CI/CD |
| 171 | +is in place. Code generation is stubbed — the `generate` command creates |
| 172 | +output directories but does not yet emit AffineScript wrappers. The |
| 173 | +Idris2 ABI proofs and Zig FFI bridge contain template placeholders |
| 174 | +awaiting domain-specific implementation. |
| 175 | + |
| 176 | +See <a href="ROADMAP.adoc" class="adoc">ROADMAP</a> for the phased |
| 177 | +development plan. |
| 178 | + |
| 179 | +# License |
| 180 | + |
| 181 | +SPDX-License-Identifier: CC-BY-SA-4.0 |
0 commit comments