Wasm linker

.gitignore

@@ -19,6 +19,9 @@ Cargo.lock
 out
 test_data/**/*.json
 
+# Local end-to-end linker scratchpad (kept locally, never committed)
+scratch/
+
 # Coverage reports
 lcov.info
 *.profraw

CHANGELOG.md

@@ -38,13 +38,77 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Language
 
+- `external fn` + `use { … } from <module>` — declare and call functions from external
+  `.wasm` libraries using logical (platform-independent) module references. The compiler
+  emits a WASM import section with one entry per bound extern; a separate link step
+  (`inference-wasm-linker`) produces a single self-contained `.wasm` and `.v` with no
+  dangling imports. Tier-A (pure) and Tier-B (caller-pointer memory) closures merge
+  automatically; Tier-C (own static data/globals/tables) produces a clear error with a
+  relocatable-build recommendation ([#9])
 - Add struct definition and parsing support ([#14])
 - Add division operator (`/`) support ([#86])
 - Add unary negation (`-`) and bitwise NOT (`~`) operators ([#86])
 - Parse visibility modifiers (`pub`) for functions, structs, enums, constants, and type aliases ([#86])
 
 ### Compiler
 
+- wasm-linker: New `core/wasm-linker` crate (`inference-wasm-linker`) implementing the
+  static-merge link pass. `link(main_wasm, &[external_wasm])` folds satisfied imports'
+  transitive closures into the main module, rewrites all index-bearing operators into a
+  unified index space, deduplicates function types, preserves the `name` custom section for
+  Rocq translation, and emits the unified WASM binary ([#9])
+- wasm-linker: External modules using **floating-point** (any `f32`/`f64` value type in a
+  signature, local, or global, or any float instruction) are now rejected by the linker. The
+  Inference language has no `f32`/`f64` types and the Rocq translator models none; floats were
+  previously admitted at the feature gate via `WASM1` but are now excluded. The feature gate
+  (`SUPPORTED_WASM_FEATURES`) is `GC_TYPES | MUTABLE_GLOBAL | BULK_MEMORY`; the safety
+  allow-list provides a second, independent backstop that rejects every float opcode with a
+  diagnostic naming the exact mnemonic (e.g. `floating-point instruction 'f32.add' is not
+  supported by the static merge`). **Sign-extension** and **saturating float-to-int** are
+  also removed from the supported set: the Rocq translator has no lowering for either, and
+  Inference codegen emits neither ([#9])
+- wasm-linker: **Tail calls** (`return_call`/`return_call_indirect`) and **segment-indexed
+  table ops** (`table.init`/`elem.drop`/`table.copy`) are rejected by the safety allow-list
+  (`UnsupportedConstruct`). The Rocq translator has no lowering for either; Inference codegen
+  never emits them, so the rejection applies only to third-party externals ([#9])
+- wasm-linker: The main-module rebuild is now fail-closed on constructs the merge cannot
+  preserve: a main module that declares a **start function**, imports **non-function
+  entities** (globals/memories/tables) from its environment, or declares a **table section**
+  is rejected up front with `UnsupportedConstruct`. Previously the start section and
+  non-function imports were silently dropped — the latter shifting the global index space so
+  `global.get` could read the wrong global — and table-using mains failed after the merge
+  with a misleading `InvalidMergedModule`. **v128** value types are likewise rejected in
+  merged signatures, locals, and block types: the Inference language has no SIMD types and
+  every SIMD operator is already rejected ([#9])
+- wasm-linker: Fixed an unsound Tier-B provenance rule. Pointer subtraction classified
+  `Param - NotParam` as still parameter-derived; because `NotParam` only means *not provably
+  parameter-derived*, the subtrahend could itself be `p - C`, so `p - (p - C) == C` fabricated
+  a fixed absolute address that the analysis accepted as caller-relative — letting a Tier-B
+  external read or write host memory outside the caller's buffer. Subtraction now preserves
+  parameter-derivation only when subtracting a provable constant (`Param - Const`), mirroring
+  the existing `add` cancellation guard. The main-module rebuild also now enforces the same
+  256-level control-flow nesting cap as the external scan and the Rocq translator, rejects a
+  duplicate `inference.spec_funcs` section instead of silently keeping only the last, rejects
+  a multi-memory main, and rejects trailing bytes in a `spec_funcs` payload ([#9])
+- wasm-linker: Merged external function names in the output name section are now
+  **module-prefixed** using a `module.field` dot convention. A closure root satisfying import
+  `sum` from logical module `mathlib` is recorded as `mathlib.sum`; an inner callee the
+  source named `helper` becomes `mathlib.helper`; a nameless callee receives a deterministic
+  fallback `mathlib.func_<idx>`. The prefix is collision-free by construction (two externals
+  bound under different logical modules can export the same field without colliding in the
+  name section). The Rocq translator sanitizes `.` to `_`, so `mathlib.sum` translates to
+  `Definition mathlib_sum` in the `.v` ([#9])
+- wasm-codegen: Emit WASM import section for `external fn` declarations. The three-stage
+  index pre-scan now runs `register_imports` before local functions, so every
+  `Def::ExternFunction` bound via `use … from` is assigned a function import index (lowest
+  indices, `0..N`), the local-function base is shifted to `N`, and extern calls lower to
+  `call <import_idx>` identically to local calls. The import section is emitted between the
+  Type and Function sections per the WASM binary format; it is omitted when there are no
+  externs. Function type deduplication (`intern_type`) ensures imports with identical
+  signatures share one type entry ([#9])
+- type-checker: `ExternOrigin { logical_module, export_field }` binds each `external fn`
+  declaration to its source module; `extern_origins()` on `SymbolTable` collects all bound
+  externs for use by codegen ([#9])
 - ast: Remove dead `OperatorKind::BitNot` variant — `~x` is always parsed as `UnaryOperatorKind::BitNot` in a `PrefixUnaryExpression`; the binary enum variant was never produced by the AST builder ([#142])
 - parser: Replace the `tree-sitter` + `tree-sitter-inference` front end with a resilient recursive-descent parser in the new `inference-parser` crate (`core/parser`). The parser lexes, parses, and lowers directly into the same `inference_ast::arena::AstArena`, producing byte-identical ASTs for all previously valid inputs, so the type-checker, analysis, codegen, and wasm-to-v phases are unchanged. The `tree-sitter`/`tree-sitter-inference` dependencies are removed from the default build, eliminating the C toolchain requirement. Parsing is now resilient (collects every syntax error instead of aborting on the first) and never panics on malformed input. `parse_external_module` moves from `inference_ast::extern_prelude` to `inference::extern_prelude` so that `inference-ast` no longer depends on the parser ([#62])
 - ast: Introduce `SimpleTypeKind` enum for primitive types, replacing string-based type matching ([#50])

Cargo.toml

@@ -34,6 +34,7 @@ inference-type-checker = { path = "./core/type-checker", version = "0.0.1" }
 inference-cli = { path = "./core/cli", version = "0.0.1" }
 inference-wasm-to-v-translator = { path = "./core/wasm-to-v", version = "0.0.1" }
 inference-wasm-codegen = { path = "./core/wasm-codegen", version = "0.0.1" }
+inference-wasm-linker = { path = "./core/wasm-linker", version = "0.0.1" }
 inference-analysis = { path = "./core/analysis", version = "0.0.1" }
 inference-compiler-interface = { path = "./core/compiler-interface", version = "0.0.1" }
 

apps/infs/src/commands/build.rs

@@ -66,6 +66,7 @@
 
 use crate::commands::project_build::{check_compiler_compatibility, mode_flag, run_project_build};
 use crate::errors::InfsError;
+use crate::project::manifest::{find_manifest_dir, InferenceToml, MANIFEST_FILE_NAME};
 use crate::project::{self, ProjectContext};
 use crate::toolchain::find_infc;
 
@@ -111,6 +112,11 @@
     /// and implies `-v`.
     #[clap(long = "mode", value_enum)]
     pub mode: Option<BuildMode>,
+
+    /// Directory to search for external `.wasm` modules referenced by
+    /// `use { … } from <module>;`. Repeatable; forwarded verbatim to `infc`.
+    #[clap(short = 'L', long = "wasm-lib-dir", value_name = "DIR")]
+    pub wasm_lib_dirs: Vec<PathBuf>,
 }
 
 /// Executes the build command with the given arguments.
@@ -175,6 +181,14 @@
         cmd.arg("--mode").arg(mode_flag(mode));
     }
 
+    for dir in &args.wasm_lib_dirs {
+        cmd.arg("--wasm-lib-dir").arg(dir);
+    }
+
+    for (name, path) in manifest_wasm_dependencies(path)? {
+        cmd.arg("--wasm-dep").arg(format_wasm_dep_arg(&name, &path)?);
+    }
+
     let status = cmd
         .stdin(std::process::Stdio::inherit())
         .stdout(std::process::Stdio::inherit())
@@ -190,6 +204,59 @@
     }
 }
 
+/// Formats one resolved manifest dependency as the `<name>=<path>` argument
+/// forwarded to `infc --wasm-dep`.
+///
+/// `name` is already validated against the logical-name grammar in
+/// [`crate::project::manifest::validate_wasm_dependency_key`], so it never
+/// contains `=`. The receiver splits on the FIRST `=`, which is therefore always
+/// the name/path boundary — a path that itself contains `=` is preserved intact.
+///
+/// The argument is a single UTF-8 `String`, so the path must round-trip through
+/// UTF-8. Using `Path::display()` would lossily substitute U+FFFD for any
+/// non-UTF-8 component and silently forward a corrupted path that resolves to the
+/// wrong file (or none). The manifest declares its paths as UTF-8 strings, so a
+/// non-UTF-8 *resolved* path can only come from a non-UTF-8 manifest directory.
+/// Reject it with an actionable error instead of corrupting it. (An
+/// OsString-preserving argument channel would lift this restriction, but is out
+/// of scope for this pass.)
+///
+/// ## Errors
+///
+/// Returns an error when `path` is not valid UTF-8.
+fn format_wasm_dep_arg(name: &str, path: &Path) -> Result<String> {
+    let Some(path) = path.to_str() else {
+        bail!(
+            "wasm dependency `{name}` resolves to a path that is not valid UTF-8 ({}); \
+             rename the containing directory to a UTF-8 path so it can be forwarded to \
+             the compiler",
+            path.display()
+        );
+    };
+    Ok(format!("{name}={path}"))
+}
+
+/// Resolves the `[wasm-dependencies]` of the project enclosing `source_path`.
+///
+/// Walks up from the source file to the nearest `Inference.toml`, loads it, and
+/// returns each declared dependency's logical name paired with its absolute
+/// `.wasm` path (relative entries resolved against the manifest directory).
+/// A source compiled outside any project (no manifest found) yields an empty
+/// list — a manifest-free build is valid and simply has no manifest deps.
+///
+/// ## Errors
+///
+/// Returns an error only if a manifest exists but cannot be read or parsed; a
+/// missing manifest is not an error.
+fn manifest_wasm_dependencies(source_path: &Path) -> Result<Vec<(String, PathBuf)>> {
+    let Some(manifest_dir) = find_manifest_dir(source_path) else {
+        return Ok(Vec::new());
+    };
+    let manifest_path = manifest_dir.join(MANIFEST_FILE_NAME);
+    let manifest = InferenceToml::from_file(&manifest_path)?;
+    manifest.resolved_wasm_dependencies(&manifest_dir)
+}
+
 /// Compiles the entry point of a discovered project (project mode).
 ///
 /// Resolves the *effective* build configuration from the CLI flags and the
@@ -271,6 +338,95 @@
     }
 }
 
+#[cfg(test)]
+mod manifest_dep_tests {
+    use super::*;
+    use assert_fs::prelude::*;
+
+    #[test]
+    fn forwards_declared_wasm_dependencies_as_absolute_paths() {
+        let temp = assert_fs::TempDir::new().unwrap();
+        let manifest = temp.child("Inference.toml");
+        manifest
+            .write_str(
+                "[package]\n\
+                 name = \"demo\"\n\
+                 version = \"0.1.0\"\n\
+                 infc_version = \"0.1.0\"\n\n\
+                 [wasm-dependencies]\n\
+                 arith = { path = \"libs/arith.wasm\" }\n",
+            )
+            .unwrap();
+        let source = temp.child("src").child("main.inf");
+        source.write_str("").unwrap();
+
+        let deps = manifest_wasm_dependencies(source.path()).expect("should resolve");
+
+        assert_eq!(deps.len(), 1);
+        assert_eq!(deps[0].0, "arith");
+        assert_eq!(deps[0].1, temp.path().join("libs/arith.wasm"));
+    }
+
+    #[test]
+    fn no_manifest_yields_no_dependencies() {
+        let temp = assert_fs::TempDir::new().unwrap();
+        let source = temp.child("main.inf");
+        source.write_str("").unwrap();
+
+        let deps = manifest_wasm_dependencies(source.path()).expect("should succeed");
+        assert!(deps.is_empty());
+    }
+
+    #[test]
+    fn manifest_without_wasm_dependencies_yields_none() {
+        let temp = assert_fs::TempDir::new().unwrap();
+        let manifest = temp.child("Inference.toml");
+        manifest
+            .write_str("[package]\nname = \"demo\"\nversion = \"0.1.0\"\ninfc_version = \"0.1.0\"\n")
+            .unwrap();
+        let source = temp.child("main.inf");
+        source.write_str("").unwrap();
+
+        let deps = manifest_wasm_dependencies(source.path()).expect("should succeed");
+        assert!(deps.is_empty());
+    }
+
+    #[test]
+    fn formats_utf8_dependency_path() {
+        let arg = format_wasm_dep_arg("arith", Path::new("/libs/arith.wasm"))
+            .expect("a UTF-8 path must format");
+        assert_eq!(arg, "arith=/libs/arith.wasm");
+    }
+
+    #[test]
+    fn preserves_equals_sign_in_path() {
+        // The receiver splits on the first `=`, so a `=` inside the path is
+        // preserved intact (the name is `=`-free by grammar validation).
+        let arg = format_wasm_dep_arg("arith", Path::new("/a=b/arith.wasm"))
+            .expect("a path containing `=` must format");
+        assert_eq!(arg, "arith=/a=b/arith.wasm");
+        assert_eq!(arg.split_once('=').map(|(n, _)| n), Some("arith"));
+    }
+
+    #[cfg(unix)]
+    #[test]
+    fn rejects_non_utf8_dependency_path() {
+        use std::os::unix::ffi::OsStrExt;
+
+        // A path component with an invalid UTF-8 byte (0xFF) cannot round-trip
+        // through the single-`String` `<name>=<path>` argument.
+        let bytes = b"/libs/\xFF/arith.wasm";
+        let path = PathBuf::from(std::ffi::OsStr::from_bytes(bytes));
+        let err = format_wasm_dep_arg("arith", &path)
+            .expect_err("a non-UTF-8 path must be rejected, not lossily forwarded");
+        let msg = err.to_string();
+        assert!(
+            msg.contains("arith") && msg.contains("not valid UTF-8"),
+            "diagnostic should name the dependency and the UTF-8 cause; got: {msg}"
+        );
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;