Wasm linker

[0xGeorgii]

Closes #9

Confidence Score: 5/5

The PR is safe to merge. The new wasm-linker is well-hardened with a fail-closed operator allow-list, a two-pass external validation gate, and extensive unit and fuzz tests covering memory reconciliation, provenance analysis, and body re-encoding edge cases.

The only finding is a dead-code guard in count_and_cap_locals that is always false after the loop above it already enforces the same cap. It carries no behavioral impact and no risk of a false pass or false rejection at runtime. All other reviewed paths are correct and well-defended.

No files require special attention. The dead-code guard in core/wasm-linker/src/provenance.rs is the only item flagged and it is non-functional.

Important Files Changed

Filename	Overview
core/wasm-linker/src/merge.rs	Core merge engine: Plan::build + emit, memory reconciliation (MemoryReconciler), type dedup, body re-encoding delegation. Well-tested and well-documented.
core/wasm-linker/src/safety.rs	Fail-closed operator allow-list; DataDrop sets only uses_data_segments (not uses_memory), which is correct since data.drop does not access linear memory bytes — consistent with tier classification.
core/wasm-linker/src/provenance.rs	Interprocedural address-provenance analysis for Tier-B soundness. count_and_cap_locals has a redundant/always-passing final guard; logic is otherwise sound.
core/wasm-linker/src/closure.rs	Transitive closure computation with effect scanning; correctly bounds control nesting and handles shared callees.
core/wasm-linker/src/rewrite.rs	Body re-encoder: remaps call/type indices, passes through main-module proof scaffolding verbatim, rejects verification-only opcodes in external bodies.
core/wasm-linker/src/tier.rs	Tier A/B/C classification; delegates memory-address soundness to provenance module; Tier C surfaces clean errors.
core/inference/src/wasm_link/driver.rs	Driver orchestration: resolves, size-caps, validates, and reads external modules; key defensive measures (TOCTOU-safe read, 64 MiB cap) are in place.
core/inference/src/wasm_link/validate.rs	Signature lowering and export-presence validation; correctly mirrors codegen's type-lowering rules.
core/wasm-linker/src/lib.rs	Public API surface and feature-set constants; documentation is comprehensive.
core/wasm-linker/src/parse.rs	Owned, section-by-section module representation; parser extracts only what the merge needs.

Sequence Diagram

sequenceDiagram
    participant CLI as infs build
    participant Driver as wasm_link/driver.rs
    participant Resolve as resolve.rs
    participant Validate as validate.rs
    participant Linker as wasm-linker/merge.rs

    CLI->>Driver: resolve_external_modules(typed_context)
    Driver->>Resolve: resolve_wasm_module(module_path)
    Resolve-->>Driver: PathBuf
    Driver->>Driver: read_external_module (size-capped)
    Driver->>Validate: validate_module_bytes (structural + feature gate)
    Validate-->>Driver: Ok / UnsupportedFeature
    Driver->>Validate: validate_extern (export + signature check)
    Validate-->>Driver: Ok / SignatureMismatch
    Driver-->>CLI: "Vec<ResolvedExternalModule>"

    CLI->>Linker: link(main_wasm, externals)
    Linker->>Linker: validate main + each external (2-pass gate)
    Linker->>Linker: Plan::build (closure, tier, memory reconcile)
    Note over Linker: closure::compute -> tier::classify -> provenance::verify_param_addressing
    Linker->>Linker: plan.emit (re-encode bodies, remap indices)
    Linker->>Linker: post-merge inf_wasmparser::validate
    Linker-->>CLI: merged .wasm bytes

Loading

_{Reviews (4): Last reviewed commit: "fix bugs" | Re-trigger Greptile}

[Copilot]

Pull request overview

This PR implements Issue #9’s external WebAssembly linking pipeline: external fn declarations can be bound to logical modules via use { … } from <module>, compiled as WASM imports, resolved/validated by the driver, and then statically merged into a single self-contained .wasm (and corresponding .v) via a new inference-wasm-linker crate.

Changes:

• Add extern provenance binding in the type-checker (ExternOrigin) and update analysis rule A024 to reject only unbound extern calls (bound externs are now supported).
• Emit WASM function imports for bound external fns in codegen (import reservation + index shifting), and add the static-merge linker (core/wasm-linker) including fuzz harnesses/tests.
• Add driver/CLI module resolution + validation + link step integration, plus Rocq-name sanitization in wasm-to-v for safer translation of arbitrary name sections.

Reviewed changes

Copilot reviewed 80 out of 95 changed files in this pull request and generated 4 comments.

Show a summary per file

File	Description
tests/test_data/inf/test_parse_source_file_1.inf	Update use … from fixture to logical-module form.
tests/test_data/inf/example.inf	Update examples to logical-module from imports.
tests/test_data/codegen/wasm/extern_import/single_import/single_import.wat	New golden WAT for single import emission.
tests/test_data/codegen/wasm/extern_import/single_import/single_import.inf	New fixture for single extern import.
tests/test_data/codegen/wasm/extern_import/multi_import/multi_import.wat	New golden WAT for multiple imports.
tests/test_data/codegen/wasm/extern_import/multi_import/multi_import.inf	New fixture for multiple extern imports.
tests/test_data/codegen/wasm/extern_import/import_with_locals/import_with_locals.wat	New golden WAT for import + locals index shifting.
tests/test_data/codegen/wasm/extern_import/import_with_locals/import_with_locals.inf	New fixture for import + locals.
tests/test_data/codegen/wasm/extern_import/import_dedup/import_dedup.wat	New golden WAT for type dedup across imports.
tests/test_data/codegen/wasm/extern_import/import_dedup/import_dedup.inf	New fixture for import signature type dedup.
tests/src/type_checker/type_checker.rs	Add extern provenance binding tests (Phase 1).
tests/src/type_checker/coverage.rs	Add extern signature validation coverage tests.
tests/src/spec_propagation.rs	Add codegen guard test for spec-name length cap.
tests/src/codegen/wasm/mod.rs	Register new extern import/link test modules.
tests/src/codegen/wasm/extern_link.rs	End-to-end link + wasm-to-v assertions.
tests/src/codegen/wasm/extern_link_exec.rs	Wasmtime execution tests to catch mis-wiring after merge.
tests/src/codegen/wasm/extern_import.rs	Golden + structural tests for import emission and call lowering.
tests/src/analysis/rules_a024.rs	Extend A024 tests for bound vs unbound extern behavior.
tests/Cargo.toml	Add wat dev-dependency for tests.
core/wasm-to-v/src/wasm_parser.rs	Sanitize function names from the WASM name section before Rocq emission.
core/wasm-to-v/src/rocq_names.rs	Add sanitize_rocq_identifier and tests.
core/wasm-to-v/README.md	Remove stale dependency mention.
core/wasm-to-v/Cargo.toml	Remove uuid dependency; add wat dev-dependency.
core/wasm-linker/src/tier.rs	Implement Tier A/B feasibility classification.
core/wasm-linker/src/spec_funcs.rs	Decode/encode and bounds-check inference.spec_funcs section.
core/wasm-linker/src/lib.rs	Public linker API + supported feature gate + errors.
core/wasm-linker/src/closure.rs	Closure computation + opcode allow-list gating + depth cap.
core/wasm-linker/README.md	Document linker design, tiers, and usage.
core/wasm-linker/fuzz/README.md	Document fuzz setup and seed corpus.
core/wasm-linker/fuzz/fuzz_targets/link.rs	libFuzzer harness for link with “Ok ⇒ validates” invariant.
core/wasm-linker/fuzz/Cargo.toml	Detached fuzz workspace configuration.
core/wasm-linker/Cargo.toml	New linker crate manifest.
core/wasm-codegen/src/spec_section.rs	Enforce spec-name length cap + tests.
core/wasm-codegen/src/lib.rs	Register imports first; validate spec-name lengths before emitting section.
core/wasm-codegen/src/errors.rs	Add UnsupportedType + SpecNameTooLong codegen errors.
core/wasm-codegen/src/compiler.rs	Implement import registration/emission + extern call lowering; add type dedup helper.
core/wasm-codegen/README.md	Update pipeline documentation for import reservation/emission.
core/wasm-codegen/docs/function-calls-lowering.md	Document three-stage index registration + extern call lowering.
core/type-checker/src/typed_context.rs	Expose extern provenance queries (extern_origin*, extern_origins, is_extern_function).
core/type-checker/src/type_checker.rs	Bind use … from to extern declarations; validate extern signatures; register externs with provenance.
core/type-checker/src/lib.rs	Re-export ExternOrigin.
core/type-checker/src/errors.rs	Add AmbiguousExternModule and ExternImportNotDeclared diagnostics + tests.
core/parser/test_data/example.inf	Update parser example fixtures for from syntax.
core/parser/src/parser.rs	Add Parser::pos() to enforce forward progress in loops.
core/parser/src/lower.rs	Lower use … from into ModuleRef segments (no string-literal paths).
core/parser/src/grammar/items.rs	Update use … from grammar; add progress guards; consume stray pub for externs.
core/parser/src/grammar.rs	Add top-level progress guard; update use … from tests; add pub external fn regression tests.
core/inference/tests/wasm_validate.rs	Integration tests for extern validation against real WASM bytes.
core/inference/tests/wasm_resolve.rs	Integration tests for logical-module resolution precedence and diagnostics.
core/inference/src/wasm_link/mod.rs	New driver-side wasm_link module exports.
core/inference/src/lib.rs	Add wasm_link module, re-export TypedContext and LinkError, add inference::link wrapper.
core/inference/Cargo.toml	Add linker + parser deps; add wasm-encoder dev-dependency.
core/cli/src/parser.rs	Add CLI flags for -L/--wasm-lib-dir and --wasm-dep.
core/cli/src/main.rs	Resolve/validate externals pre-codegen; invoke link step; handle post-link spec-func indices.
core/ast/src/nodes.rs	Replace UseDirective.from: Option<String> with Option<ModuleRef>.
core/ast/docs/nodes.md	Update AST docs for UseDirective + ModuleRef.
core/analysis/src/walker.rs	Add walk_block_stmts helper for per-body traversals.
core/analysis/src/rules/extern_function_call.rs	Update A024 to be scope-aware and reject only unbound extern calls.
CHANGELOG.md	Document new extern/WASM linking feature set.
Cargo.toml	Add inference-wasm-linker to workspace deps.
book/src/SUMMARY.md	Add book chapter for extern/WASM linking.
book/src/external-functions-and-wasm-linking.md	New user documentation for externs/linking.
apps/infs/tests/fixtures/example.inf	Update fixture to logical-module from imports.
apps/infs/tests/cli_integration.rs	Minor refactor: use is_ok_and.
apps/infs/src/commands/build.rs	Forward --wasm-lib-dir and manifest deps to infc; add manifest dep tests.
.gitignore	Ignore local scratch/ directory.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[codecov]

Codecov Report

❌ Patch coverage is 90.63318% with 537 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
core/wasm-linker/src/merge.rs	87.75%	104 Missing ⚠️
core/wasm-linker/src/safety.rs	79.60%	94 Missing ⚠️
core/wasm-linker/src/provenance.rs	87.20%	93 Missing ⚠️
core/type-checker/src/symbol_table.rs	81.68%	50 Missing ⚠️
core/inference/src/wasm_link/driver.rs	80.78%	39 Missing ⚠️
core/wasm-to-v/src/translator.rs	82.16%	28 Missing ⚠️
core/type-checker/src/type_checker.rs	85.21%	21 Missing ⚠️
core/cli/src/main.rs	86.29%	17 Missing ⚠️
core/type-checker/src/errors.rs	59.52%	17 Missing ⚠️
core/wasm-linker/src/parse.rs	95.76%	15 Missing ⚠️
... and 12 more

📢 Thoughts on this report? Let us know!

[Copilot]

Pull request overview

Copilot reviewed 80 out of 95 changed files in this pull request and generated 1 comment.

[Copilot]

Pull request overview

Copilot reviewed 80 out of 95 changed files in this pull request and generated 2 comments.

[Copilot]

Pull request overview

Copilot reviewed 80 out of 95 changed files in this pull request and generated 1 comment.

[Copilot]

Pull request overview

Copilot reviewed 80 out of 95 changed files in this pull request and generated 2 comments.

[Copilot]

Pull request overview

Copilot reviewed 80 out of 95 changed files in this pull request and generated no new comments.