Skip to content

Commit 1be936e

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
chore(floor-raise): add integration files (Phase 2)
Add proven, verisimdb, feedback-o-tron, and vexometer integration manifests as part of Floor Raise campaign Phase 2. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 80fa2f8 commit 1be936e

8 files changed

Lines changed: 1230 additions & 378 deletions

File tree

‎README.adoc‎

Lines changed: 162 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -4,40 +4,183 @@
44
Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
55
:toc: left
66
:icons: font
7+
:source-highlighter: rouge
78

8-
== What Is This?
9+
== What Is Affinescriptiser?
910

10-
AffineScriptiser wraps existing code in **affine types, dependent types, and
11-
algebraic effects** — compiling to WebAssembly with no garbage collector.
11+
Affinescriptiser takes existing code written in Rust, C, or Zig and wraps it with
12+
https://github.com/hyperpolymath/affinescript[AffineScript]'s type system -- combining
13+
**affine types** (resources used at most once) with **dependent types** (compile-time
14+
value constraints) -- then compiles the result to **WebAssembly**.
1215

13-
AffineScript combines Rust's ownership model with Idris-level dependent types
14-
and Koka-style effects. AffineScriptiser makes this accessible to existing codebases.
16+
The outcome: resources such as file descriptors, sockets, GPU buffers, and heap
17+
allocations become *provably* safe. They cannot be leaked, double-freed, or used
18+
after release. The wrapped code ships as a `.wasm` binary with zero garbage collector
19+
and zero runtime overhead from the type proofs.
20+
21+
Affinescriptiser is part of the https://github.com/hyperpolymath/iseriser[-iser family],
22+
a collection of tools that wrap existing code in a target language's capabilities
23+
without requiring users to learn that language.
1524

1625
== How It Works
1726

18-
Describe your interface contracts in `affinescriptiser.toml`. AffineScriptiser:
27+
You describe your code in an `affinescriptiser.toml` manifest, point at your source
28+
files, and declare which resources need affine tracking.
1929

20-
1. Analyses your function signatures and resource patterns
21-
2. Generates AffineScript wrappers with ownership + dependent type contracts
22-
3. Compiles to WebAssembly (no GC, no runtime, minimal binary)
23-
4. Creates FFI bridges for calling from JavaScript, Rust, or C
30+
[source,toml]
31+
----
32+
# affinescriptiser.toml — example manifest
33+
[workload]
34+
name = "secure-file-processor"
35+
entry = "src/lib.rs::process_file"
36+
strategy = "affine-wrap"
2437
25-
== Key Value
38+
[data]
39+
input-type = "FileHandle"
40+
output-type = "ProcessedResult"
41+
42+
[options]
43+
flags = ["track-file-descriptors", "track-allocations", "wasm-size-opt"]
44+
----
45+
46+
Affinescriptiser then:
2647

27-
* **Rust-level safety + Idris-level verification** → WASM
28-
* **Dependent type contracts** verified at compile time
29-
* **Algebraic effects** for clean error handling and IO
30-
* **Zero-GC WebAssembly** — tiny, fast, portable binaries
48+
1. **Analyses** your function signatures and identifies resource handles
49+
(file descriptors, heap allocations, locks, GPU buffers)
50+
2. **Generates** AffineScript type annotations that enforce at-most-once usage
51+
for each tracked resource
52+
3. **Proves** via Idris2 that affine invariants hold across the FFI boundary
53+
4. **Compiles** the wrapped code to WebAssembly with size and performance
54+
optimisation
3155

3256
== Architecture
3357

34-
Follows the hyperpolymath -iser pattern:
35-
manifest -> Idris2 ABI proof -> Zig FFI bridge -> target language codegen.
36-
Part of the https://github.com/hyperpolymath/iseriser[-iser family].
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+
[cols="1,3"]
86+
|===
87+
| Layer | Role
88+
89+
| **Manifest** (`affinescriptiser.toml`)
90+
| User declares what code to wrap and which resources to track.
91+
92+
| **Source Analysis** (Rust, `src/manifest/`, `src/codegen/`)
93+
| Parses input source files, identifies resource handles and ownership patterns.
94+
95+
| **Idris2 ABI** (`src/interface/abi/`)
96+
| Formal proofs that affine invariants (at-most-once usage, no leaks) hold.
97+
Defines `ResourceKind`, `Linearity`, `Ownership`, and WASM memory layout.
98+
99+
| **Zig FFI** (`src/interface/ffi/`)
100+
| C-ABI compatible bridge between the proven ABI and the generated code.
101+
Zero runtime overhead, cross-compilation built in.
102+
103+
| **AffineScript Codegen** (`src/codegen/`)
104+
| Generates AffineScript wrapper code with ownership annotations and
105+
algebraic effect handlers. Compiles to WASM.
106+
107+
| **WASM Output**
108+
| Final `.wasm` binary. No garbage collector, no runtime, minimal size.
109+
|===
110+
111+
== Key Value
112+
113+
**Automatic resource safety** -- files, sockets, GPU buffers, and heap allocations
114+
cannot be leaked or double-freed. The type system proves this at compile time, not
115+
at runtime.
116+
117+
**WASM deployment** -- the output is a portable WebAssembly binary that runs in
118+
browsers, edge workers, IoT devices, or any WASM runtime. No GC means predictable
119+
latency and tiny binary size.
120+
121+
**Zero target-language exposure** -- users never write AffineScript directly. They
122+
describe their intent in TOML and let affinescriptiser handle the wrapping, proving,
123+
and compilation.
124+
125+
== Use Cases
126+
127+
* **Browser sandboxed computation** -- run resource-safe code in the browser via WASM
128+
without worrying about memory leaks in long-running tabs
129+
* **Edge computing** -- deploy provably-safe WASM modules to Cloudflare Workers,
130+
Fastly Compute, or Deno Deploy with guaranteed resource bounds
131+
* **IoT firmware** -- compile to WASM for microcontrollers with formal proof that
132+
bounded memory is respected
133+
* **GPU buffer management** -- wrap CUDA/Vulkan buffer allocations with affine types
134+
to prevent double-free and use-after-free in compute shaders
135+
* **Secure file processing** -- process sensitive files with compile-time proof that
136+
file handles are closed exactly once
137+
138+
== CLI Commands
139+
140+
[source,bash]
141+
----
142+
# Initialise a new manifest in the current directory
143+
affinescriptiser init
144+
145+
# Validate your manifest
146+
affinescriptiser validate -m affinescriptiser.toml
147+
148+
# Generate AffineScript wrappers, Zig FFI bridge, and C headers
149+
affinescriptiser generate -m affinescriptiser.toml -o generated/affinescriptiser
150+
151+
# Build the generated artifacts
152+
affinescriptiser build -m affinescriptiser.toml --release
153+
154+
# Run the workload
155+
affinescriptiser run -m affinescriptiser.toml -- --input data.bin
156+
157+
# Show manifest information
158+
affinescriptiser info -m affinescriptiser.toml
159+
----
160+
161+
== Building from Source
162+
163+
[source,bash]
164+
----
165+
# Prerequisites: Rust (nightly), Idris2, Zig
166+
cargo build --release
167+
168+
# Run tests
169+
cargo test
170+
171+
# Full quality check (format, lint, test)
172+
just quality
173+
----
37174

38175
== Status
39176

40-
**Pre-alpha.** Architecture defined, scaffolding in place, codegen pending.
177+
**Pre-alpha / Scaffold.** The architecture is defined, the CLI is functional (init,
178+
validate, info), and the RSR template with full CI/CD is in place. Code generation
179+
is stubbed -- the `generate` command creates output directories but does not yet emit
180+
AffineScript wrappers. The Idris2 ABI proofs and Zig FFI bridge contain template
181+
placeholders awaiting domain-specific implementation.
182+
183+
See link:ROADMAP.adoc[ROADMAP.adoc] for the phased development plan.
41184

42185
== License
43186

‎ROADMAP.adoc‎

Lines changed: 107 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -1,32 +1,111 @@
11
// SPDX-License-Identifier: PMPL-1.0-or-later
2-
= affinescriptiser Roadmap
3-
:toc:
2+
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
= Affinescriptiser Roadmap
4+
Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
5+
:toc: left
46
:icons: font
57

68
== Phase 0: Scaffold (COMPLETE)
7-
* [x] RSR template with full CI/CD
8-
* [x] CLI with subcommands
9-
* [x] Manifest parser
10-
* [x] Codegen stubs
11-
* [x] ABI module stubs
12-
* [x] README with architecture
13-
14-
== Phase 1: Core Implementation
15-
* [ ] Implement target-language-specific code generation
16-
* [ ] Write Idris2 ABI proofs for core invariants
17-
* [ ] Build Zig FFI bridge
18-
* [ ] First working end-to-end example
19-
* [ ] Integration tests
20-
21-
== Phase 2: Polish
22-
* [ ] Error messages and diagnostics
23-
* [ ] Shell completions (bash, zsh, fish)
24-
* [ ] CI/CD for the generated artifacts
25-
* [ ] Performance benchmarks
26-
* [ ] Additional examples
27-
28-
== Phase 3: Ecosystem
29-
* [ ] PanLL panel integration
30-
* [ ] BoJ-server cartridge
31-
* [ ] VeriSimDB backing store for results
32-
* [ ] Publish to crates.io
9+
10+
* [x] RSR template with full CI/CD (17 workflows)
11+
* [x] Rust CLI with subcommands (init, validate, generate, build, run, info)
12+
* [x] Manifest parser (`affinescriptiser.toml` → `Manifest` struct)
13+
* [x] Codegen module stubs (`src/codegen/mod.rs`)
14+
* [x] Idris2 ABI template files (Types.idr, Layout.idr, Foreign.idr)
15+
* [x] Zig FFI template files (build.zig, main.zig, integration_test.zig)
16+
* [x] README with architecture diagram
17+
* [x] Machine-readable metadata (STATE.a2ml, META.a2ml, ECOSYSTEM.a2ml)
18+
19+
== Phase 1: Source Analysis
20+
21+
Parse Rust, C, and Zig source files to identify resource handles that need
22+
affine tracking.
23+
24+
* [ ] Rust source parser -- identify types implementing `Drop`, `File`, `TcpStream`,
25+
`MutexGuard`, raw pointers with paired `alloc`/`dealloc`
26+
* [ ] C source parser -- identify `FILE *`, `malloc`/`free` pairs, `open`/`close`
27+
pairs, `pthread_mutex_lock`/`unlock`
28+
* [ ] Zig source parser -- identify `std.mem.Allocator` usage, `defer` patterns,
29+
error union return types
30+
* [ ] Resource handle registry -- canonical map of (handle type, acquire fn, release fn)
31+
extracted from source analysis
32+
* [ ] Manifest enrichment -- `affinescriptiser.toml` gains `[resources]` section where
33+
users can override or supplement auto-detected resource handles
34+
* [ ] First end-to-end example: wrap a Rust file processor so `FileHandle` is
35+
affine-tracked through to WASM output
36+
37+
== Phase 2: Affine Wrapping
38+
39+
Generate AffineScript type annotations that enforce at-most-once usage for
40+
every tracked resource.
41+
42+
* [ ] AffineScript AST builder -- programmatically construct `affine T`, `linear T`,
43+
and `dependent (n : Nat) -> Vec n T` annotations
44+
* [ ] Ownership graph -- build a directed graph of resource ownership transfers and
45+
verify it is acyclic
46+
* [ ] Drop insertion -- automatically insert resource release calls at scope exit
47+
for affine-typed values
48+
* [ ] Effect handler generation -- generate algebraic effect handlers for IO, file
49+
operations, and network calls
50+
* [ ] Error path analysis -- prove that resources are released on *every* error path,
51+
not just the happy path
52+
* [ ] Codegen integration -- wire the AST builder into `src/codegen/mod.rs` so
53+
`affinescriptiser generate` emits real AffineScript source
54+
55+
== Phase 3: WASM Compilation
56+
57+
Compile the wrapped code to `.wasm` with size and performance optimisation.
58+
59+
* [ ] AffineScript-to-WASM backend -- lower AffineScript AST to WASM instructions
60+
* [ ] Size optimisation -- dead code elimination, function merging, wasm-opt passes
61+
* [ ] Memory model -- linear memory layout matching Idris2 `Layout.idr` proofs,
62+
no GC, stack-based allocation where possible
63+
* [ ] WASI support -- optional WASI imports for file I/O, clocks, random
64+
* [ ] Multi-target -- `wasm32-unknown-unknown` (browser), `wasm32-wasi` (server/edge),
65+
`wasm32-unknown-emscripten` (legacy)
66+
* [ ] Binary size budget -- target <50KB for a minimal affine-wrapped function,
67+
<200KB for a full file processor
68+
* [ ] Performance benchmarks -- compare latency and throughput against native Rust
69+
and against untyped WASM
70+
71+
== Phase 4: Idris2 Formal Proofs
72+
73+
Replace template placeholders with domain-specific proofs that affine invariants
74+
hold across the FFI boundary.
75+
76+
* [ ] `ResourceKind` -- prove completeness: every detected resource handle maps to
77+
exactly one `ResourceKind` variant
78+
* [ ] `Linearity` proof -- prove that for every `affine T` annotation, the generated
79+
code uses `T` at most once on every execution path
80+
* [ ] `Ownership` transfer proof -- prove that ownership graph edges preserve
81+
linearity (no aliasing of affine resources)
82+
* [ ] WASM memory layout proof -- prove that `Layout.idr` field offsets match the
83+
actual WASM linear memory layout emitted by Phase 3
84+
* [ ] FFI boundary proof -- prove that every C-ABI function in `Foreign.idr` correctly
85+
translates affine ownership semantics across the Zig FFI bridge
86+
* [ ] Regression proof suite -- automated CI check that proofs still hold after
87+
codegen changes
88+
89+
== Phase 5: Ecosystem Integration
90+
91+
* [ ] **BoJ cartridge** -- package affinescriptiser as a BoJ-server cartridge for
92+
on-demand affine wrapping via MCP
93+
* [ ] **PanLL panel** -- affinescriptiser panel showing resource ownership graph,
94+
affine violation diagnostics, and WASM binary size breakdown
95+
* [ ] **IDE integration** -- LSP-compatible diagnostics for affine violations
96+
(red squiggles on double-use, yellow on potential leak)
97+
* [ ] **iseriser integration** -- register affinescriptiser in the meta-framework so
98+
`iseriser new affinescript <name>` scaffolds a project
99+
* [ ] **VeriSimDB backing** -- store analysis results, proof artefacts, and WASM
100+
binaries in VeriSimDB for reproducible builds
101+
* [ ] **crates.io publish** -- release affinescriptiser CLI to crates.io
102+
* [ ] **WASM package registry** -- publish generated `.wasm` modules to WAPM or
103+
a custom registry
104+
105+
== Non-Goals
106+
107+
* Affinescriptiser does *not* implement a general-purpose AffineScript compiler.
108+
It generates targeted wrappers for existing code.
109+
* Affinescriptiser does *not* support languages beyond Rust, C, and Zig as input.
110+
Other -iser tools handle other source languages.
111+
* Affinescriptiser does *not* provide a runtime. The output is a static WASM binary.

0 commit comments

Comments
 (0)