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