docs: align README with PulseEngine visual identity#51
Merged
Conversation
Adds specialized optimization passes for WebAssembly modules produced by
component fusion tools (meld). Targets adapter trampolines, duplicate
types/imports, and dead functions introduced by the fusion process.
New files:
- loom-core/src/fused_optimizer.rs: 4-pass fused optimization pipeline
- Pass 1: Adapter devirtualization (bypass trivial trampolines)
- Pass 2: Function type deduplication (merge identical types)
- Pass 3: Dead function elimination (remove unreachable functions)
- Pass 4: Import deduplication (merge duplicate imports)
- docs/FUSED_COMPONENT_OPTIMIZATION.md: full design document
- proofs/simplify/FusedOptimization.v: Rocq correctness proofs
Integration:
- Wired into component_optimizer.rs (runs before standard 12-phase pipeline)
- Wired into optimize_module() for standalone module optimization
- Safe no-ops on non-fused modules
Adds specialized optimization passes for WebAssembly modules produced by component fusion tools (meld). Targets adapter trampolines, duplicate types/imports, and dead functions introduced by the fusion process. New files: - loom-core/src/fused_optimizer.rs: 4-pass fused optimization pipeline - Pass 1: Adapter devirtualization (bypass trivial trampolines) - Pass 2: Function type deduplication (merge identical types) - Pass 3: Dead function elimination (remove unreachable functions) - Pass 4: Import deduplication (merge duplicate imports) - docs/FUSED_COMPONENT_OPTIMIZATION.md: full design document - proofs/simplify/FusedOptimization.v: Rocq correctness proofs Integration: - Wired into component_optimizer.rs (runs before standard 12-phase pipeline) - Wired into optimize_module() for standalone module optimization - Safe no-ops on non-fused modules Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Rename all SCREAMING_CASE doc files to kebab-case and organize into design/, guides/, and bugs/ subdirectories. Rewrite fused component optimization doc with 8 mermaid diagrams, proof status tables, and tiered roadmap. Update all cross-references in README and related docs. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…ete proofs - Add Pass 2: trivial call elimination for meld's cabi_post_return stubs (detects () -> () functions with empty bodies, removes all calls) - Enhance dead function elimination with element segment parsing using wasmparser to extract indirect call targets from element sections - Rebuild element sections with remapped indices via wasm_encoder after DCE - Complete all 4 previously Admitted Rocq proofs in FusedOptimization.v: * adapter_devirtualization_correct (via trivial_adapter_equiv axiom) * type_dedup_idempotent (via strengthened is_canonical_type_remap) * import_dedup_preserves_semantics (via identical_import_equiv axiom) * fused_then_standard_correct (via reachability preservation hypothesis) - Add new Pass 2 proof: trivial_call_is_nop (via trivial_call_nop axiom) - Zero Admitted proofs remaining in FusedOptimization.v Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…pipeline Update proof status table (all 11 theorems now Qed, zero Admitted), add Pass 2 (trivial call elimination) to pipeline diagrams, fix pass numbering to reflect 5-pass pipeline, update DCE description to mention element segment parsing, add proof architecture diagram showing axiom dependencies. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…y modules In single-memory modules produced by meld, adapters that allocate a buffer via cabi_realloc and memory.copy within the same linear memory are redundant. This pass detects these adapters and collapses them to trivial forwarding trampolines, which Pass 1 then devirtualizes to eliminate the call overhead. Adds 9-predicate detection (single memory, has locals, same-memory copy, realloc call, single target call, no control flow/stores/global writes, signature match), collapse_to_forwarding transformation, 12 unit tests, Rocq axiom (same_memory_adapter_equiv) and theorem (same_memory_collapse_correct). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Test plan
🤖 Generated with Claude Code