Skip to content

Commit c6649c6

Browse files
hyperpolymathhyperpolymath
committed
Add sponsor badge
1 parent cd3a8be commit c6649c6

1 file changed

Lines changed: 189 additions & 0 deletions

File tree

‎README.md‎

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

0 commit comments

Comments
 (0)