Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .machine_readable/6a2/ECOSYSTEM.a2ml
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,6 @@ notes = "Ephapax provides the resource-safety guarantees (no-leak, no-use-after-
projects = [
{ name = "proven", relationship = "downstream-consumer", notes = "Proven consumes ephapax via Zig bindings for high-assurance resource management." },
{ name = "007-lang", relationship = "sibling-language", notes = "Shares linear logic concepts for agent handles and session types." },
{ name = "typed-wasm", relationship = "aggregate-library", notes = "Shared binary layout conventions for WasmGC cross-language calls." },
{ name = "typed-wasm", relationship = "code-dependency", notes = "ephapax-wasm + ephapax-cli depend on `crates/typed-wasm-verify` (Cargo git dep, pinned by rev) for L7 (aliasing) + L10 (linearity) post-codegen verification. ephapax emits the `affinescript.ownership` custom section on every compile (C6); `ephapax compile --verify-ownership` runs the verifier on the emitted module (C7). Shared binary layout conventions for cross-language calls remain a longer-term concern." },
{ name = "standards", relationship = "parent", notes = "Enforces the RSR 2026 standards that ephapax implements." },
]
4 changes: 4 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,10 @@ All notable changes to Ephapax are documented here.
## [Unreleased]

### Added
- **typed-wasm L7+L10 integration** (closes the typed-wasm-verify loop for ephapax):
- **C6 (#70)** — `ephapax-wasm` emits an `affinescript.ownership` custom section on every compile when any user fn has a Linear parameter. Section format and encoder come from the new `typed-wasm-verify` Rust crate (`hyperpolymath/typed-wasm:crates/typed-wasm-verify/`, rev `e11bb985` at C6, bumped to `67006edd` at C7). Driven by `Ty::is_linear()`; entries sorted by `func_idx` for deterministic output. 4 new unit tests; `cargo test --workspace` clean.
- **C7 (#72)** — New `--verify-ownership` flag on `ephapax compile`. After codegen and before output write, runs `typed_wasm_verify::verify_from_module` on the emitted module and surfaces any aliasing / linearity violation as a non-zero exit. Output: `✓ typed-wasm L7+L10 verification: clean` on success; per-violation diagnostics on failure. 3 new integration tests spawn the built binary.
- Net effect: ephapax-emitted wasm now has end-to-end L7+L10 guarantees — producer side (custom section emission) + opt-in consumer side (verifier flag), both backed by the canonical Rust verifier shared with `hyperpolymath/typed-wasm`.
- `module Qualified.Name` declarations (dotted module paths)
- `--` Haskell-style line comments (alongside existing `//` and `/* */`)
- Qualified names in imports: `import Foo.Bar.Baz`
Expand Down
Loading