Skip to content

ROADMAP.adoc

Latest commit

 

History

History
73 lines (59 loc) · 3.54 KB

ROADMAP.adoc

File metadata and controls

73 lines (59 loc) · 3.54 KB
Raw

ephapaxiser Roadmap

Table of Contents

Phase 0: Scaffold (COMPLETE)

  • ✓ RSR template with full CI/CD (17 workflows)

  • ✓ Rust CLI with subcommands (init, validate, generate, build, run, info)

  • ✓ Manifest parser (ephapaxiser.toml)

  • ✓ Codegen stubs (output directory creation, placeholder messages)

  • ✓ Idris2 ABI module stubs (Types.idr, Layout.idr, Foreign.idr)

  • ✓ Zig FFI bridge stubs (main.zig, build.zig, integration tests)

  • ✓ README with architecture overview

Phase 1: Resource Detection

  • ❏ Parse source files to identify resource acquisition patterns (open/close, connect/disconnect, alloc/free, acquire/release)

  • ❏ Build resource handle registry from analysis results

  • ❏ Detect paired operations (acquire/release) and orphaned resources

  • ❏ Output resource graph: which handles flow where and when they are consumed

  • ❏ Support Rust, C, and Zig source files as analysis targets

  • ❏ Integration tests with sample codebases containing known resource leaks

Phase 2: Ephapax Wrapper Generation

  • ❏ Generate Ephapax linear type wrappers for each detected resource class

  • ❏ Enforce single-use semantics: each wrapper value must be consumed exactly once

  • ❏ Emit target-language glue code (Rust, C, Zig) that wraps original handles

  • ❏ Template-driven codegen via Handlebars (already a dependency)

  • ❏ First working end-to-end example: file handle wrapper with compile-time leak detection

Phase 3: Linearity Enforcement

  • ❏ Compile-time enforcement that wrapped resources are consumed exactly once

  • ❏ Diagnostic messages: clear errors for use-after-consume, leaked resources, double-free attempts

  • ❏ Support for resource transfer (move semantics through function boundaries)

  • ❏ Support for conditional consumption (if-then-else where both branches consume)

  • ❏ WASM target: proofs erased at compile time, zero runtime overhead

Phase 4: Idris2 Proofs of Resource Safety

  • ❏ LinearResource type in Types.idr: dependent type encoding single-use semantics

  • ❏ UsageCount proof: compile-time counter proving usage == 1

  • ❏ ResourceLifecycle state machine: acquired → in-use → consumed (no other transitions)

  • ❏ ConsumeProof witness: evidence that a resource was properly consumed

  • ❏ Memory layout proofs in Layout.idr for resource tracking structs

  • ❏ FFI declarations in Foreign.idr for resource analysis operations

  • ❏ Idris2 wins rule: if proofs conflict with Ephapax wrappers, adjust the wrappers — never the proofs

Phase 5: Multi-Language Support (Rust / C / Zig)

  • ❏ Rust: generate Drop-based wrappers that enforce linear consumption

  • ❏ C: generate header + source pairs with attributecleanup enforcement

  • ❏ Zig: generate comptime-checked wrappers leveraging Zig’s defer and error unions

  • ❏ Cross-language interop: resources created in one language, consumed in another

  • ❏ Platform-specific codegen (Linux, macOS, Windows, WASM)

Phase 6: Ecosystem Integration

  • ❏ PanLL panel integration (resource lifecycle visualisation)

  • ❏ BoJ-server cartridge for ephapaxiser operations

  • ❏ VeriSimDB backing store for analysis results and proof artifacts

  • ❏ Error messages and diagnostics polish

  • ❏ Shell completions (bash, zsh, fish)

  • ❏ CI/CD for generated artifacts

  • ❏ Performance benchmarks

  • ❏ Publish to crates.io

  • ❏ Additional examples: database connections, GPU buffers, session tokens, crypto keys