Feat/wasm opt post build

.gitignore

@@ -41,6 +41,7 @@ external/
 !CHANGELOG.md
 *.vsix
 editors/vscode/package-lock.json
+editors/vscode/node_modules/
 
 # mdBook render output
 /book/book/

CHANGELOG.md

@@ -627,6 +627,23 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### infs CLI
 
+- Add opt-in post-build WASM optimization via Binaryen `wasm-opt`
+  - After a successful project-mode `infs build`/`infs run`, when the manifest declares `[build.wasm-opt]`, the external `wasm-opt` binary optimizes `out/main.wasm` in place; absent the table, the pipeline is unchanged
+  - Runs only for executable artifacts: proof-mode builds and any `-v` build are always skipped silently, since their WASM can carry non-deterministic opcodes (`forall`/`exists`/`assume`/`unique`/`@` uzumaki) that `wasm-opt` cannot parse
+  - A compile-mode artifact that still contains a non-deterministic opcode is a hard error naming the construct and pointing at the fix (move it into a `spec` block, or disable optimization), rather than an opaque `wasm-opt` parse failure
+  - `infs run` applies the same optimization as `infs build`, so it always executes exactly what a build would ship; single-file mode is unaffected
+  - New `--no-wasm-opt` flag on `infs build` and `infs run` skips optimization for a single invocation regardless of the manifest
+  - `wasm-opt` is resolved via the `WASM_OPT_PATH` environment variable, falling back to PATH, then an infs-managed Binaryen install (see below); if none resolves, the build fails with install hints led by `infs component add wasm-opt`
+  - The resolved binary must be Binaryen 116 or newer; an older version is a hard error, while an unparseable `--version` output only warns and proceeds
+  - `wasm-opt` strips the WASM names custom section, so stack traces from an optimized artifact lose function names
+- Add infs-managed Binaryen provisioning for `wasm-opt` (`infs component`)
+  - New `infs component add|list|remove <name>` command family (rustup-style) manages optional toolchain components, a tier distinct from the `infc` toolchain install; `wasm-opt` (Binaryen) is the only component today
+  - `infs component add wasm-opt` downloads a pinned, sha256-verified Binaryen release (`version_130`) into `~/.inference/tools/binaryen/<version>/`; the checksum is verified before anything reaches the install directory, the install is idempotent (no network access when already installed) and atomic (staged under a per-process temp directory, published with a single rename), and a broken prior install is repaired rather than left stale
+  - `infs component list` reports each component's install state and location; `infs component remove wasm-opt` deletes the managed install; `add` prints a note when `WASM_OPT_PATH` or a PATH `wasm-opt` would shadow the newly installed managed copy at build time
+  - `wasm-opt` resolution gains a third precedence tier — `WASM_OPT_PATH` env → PATH → the managed install — completing a chain that previously hard-errored whenever the first two missed; set `INFS_VERBOSE=1` to trace which tier resolved the binary
+  - New `[build.wasm-opt] auto-install` manifest key (default `false`): when `true` and `wasm-opt` resolves in no tier, `infs` downloads the pinned Binaryen at build time instead of erroring
+  - The missing-`wasm-opt` install-hint error now leads with `infs component add wasm-opt`, ahead of the brew/apt/npm/releases hints, and mentions `auto-install = true` as the hands-off alternative
+  - `infs doctor` gains an appended `wasm-opt` check: OK naming the resolved path, precedence tier, and Binaryen version (noting when a managed copy is shadowed by PATH); an unused `wasm-opt` reports OK as "not installed (optional)" rather than alarming projects that don't use `[build.wasm-opt]`; a broken managed install, a failing `--version` probe, or an invalid `WASM_OPT_PATH` each WARN with remediation
 - Make `infs build` and `infs run` project-aware ([#223])
   - Invoked with no path, both commands discover the project's `Inference.toml` by walking up from the current directory (nearest ancestor wins; the start directory is canonicalized once for symlink stability), then compile `<root>/src/main.inf` with the compiler's working directory set to the project root so `out/` always lands at the root regardless of where the command was invoked
   - The existing single-file forms (`infs build path/to/file.inf`, `infs run path/to/file.inf`) are preserved unchanged
@@ -714,6 +731,11 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Project Manifest
 
+- Add optional `[build.wasm-opt]` sub-table to `Inference.toml`
+  - `enabled` (bool, default `true`): table presence alone enables optimization; set `enabled = false` to keep the table while disabling the step
+  - `level` (string, default `"3"`): forwarded to `wasm-opt` as `-O<level>`; one of `"0"`–`"4"`, `"s"`, `"z"`, validated on load with a clear error naming the offending value
+  - `auto-install` (bool, default `false`): downloads a missing `wasm-opt` automatically at build time — the same pinned, checksum-verified Binaryen `infs component add wasm-opt` installs — instead of hard-erroring; recorded in the versioned manifest since `infs` has no interactive prompts
+  - `infs new`/`infs init` scaffold a commented-out `[build.wasm-opt]` block after `[build]`, including an `# auto-install = true` line
 - Consume `[build]` and `[verification]` configuration in project-mode builds ([#223])
   - New `[build] mode = "compile" | "proof"` field (default `"compile"`), validated on load; an invalid value is a clear error naming the field and allowed values
   - `[verification] output-dir` is honored only in effective-proof builds, where it redirects artifacts via `infc --out-dir`; in compile mode it is ignored so the default `proofs/` never relocates `out/main.wasm`
@@ -757,6 +779,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   - Simplify `buildFakeInfcArchive()` to emit only `infc` binary
   - Update doctor check expectations from 6 to 5 checks (single `infc` check replaces `inf-llc`, `rust-lld`, `libLLVM`)
   - Change "missing lib directory triggers doctor warning" to "missing infc triggers doctor failure"
+- Add "Install Component (wasm-opt)" command to VS Code extension (`inference.installComponent`)
+  - Runs `infs component add <name>` with a progress notification; refreshes `infs doctor` on success; offers Show Output / Retry actions on failure
+  - `infs doctor` notifications (error and warning toasts alike) gain an "Install wasm-opt" action button whenever a `wasm-opt` check reports a warning or failure, invoking the install command directly
 
 ---
 

apps/infs/Cargo.toml

@@ -35,6 +35,7 @@ crossterm = "0.29.0"
 anyhow.workspace = true
 thiserror.workspace = true
 inference-compiler-interface.workspace = true
+inf-wasmparser.workspace = true
 
 [target.'cfg(windows)'.dependencies]
 winreg = "0.56"
@@ -45,6 +46,10 @@ predicates = "3.1.3"
 assert_fs = "1.1.1"
 serial_test = "3.2"
 regex = "1"
+wasm-encoder = "0.249.0"
+tar = "0.4"
+flate2 = "1"
+sha2 = "0.11"
 
 [profile.release]
 opt-level = "z"       # Optimize for size (not speed)

apps/infs/README.md

@@ -51,6 +51,9 @@ cargo build -p infs --release
 | `infs default <version>` | Set the default toolchain |
 | `infs doctor` | Check installation health with intelligent recommendations |
 | `infs self update` | Update infs itself |
+| `infs component add <name>` | Install a managed component (currently `wasm-opt`, the Binaryen optimizer behind `[build.wasm-opt]`) |
+| `infs component list` | List managed components and their install state |
+| `infs component remove <name>` | Remove an installed managed component |
 
 ### Other
 
@@ -106,20 +109,22 @@ infs build example.inf --analyze
 | `-v` | Generate Rocq (.v) translation file |
 | `--mode proof` | Proof mode: preserve non-det specs; implies `-v` inside `infc` |
 | `--mode compile` | Compile mode: strip specs for executable WASM |
+| `--no-wasm-opt` | Skip `[build.wasm-opt]` post-build optimization (project mode only) |
 
 When no phase flag is given, `infs build` defaults to full compilation and writes the WASM binary to disk — equivalent to `--codegen -o`.
 
 ### Project-mode Manifest Semantics
 
-When `infs build` runs in project mode, it reads two fields from `Inference.toml` to resolve the build configuration:
+When `infs build` runs in project mode, it reads fields from `Inference.toml` to resolve the build configuration:
 
 | Manifest field | Effect |
 |----------------|--------|
 | `[build] mode = "proof"` | Forwards `--mode proof` to `infc`; activates `output-dir` |
 | `[build] mode = "compile"` (default) | Forwards nothing; `infc` defaults to compile mode |
 | `[verification] output-dir` | Honored only in effective-proof mode; relocates both `.wasm` and `.v` |
+| `[build.wasm-opt]` | Opt-in post-build optimization of `out/main.wasm` via Binaryen `wasm-opt`, resolved from `WASM_OPT_PATH` → PATH → an infs-managed install; absent table is a no-op |
 
-CLI flags always override manifest settings. `infs run` ignores `[build] mode` entirely and always builds an executable in `out/` (proof-mode WASM contains non-deterministic opcodes that `wasmtime` cannot execute).
+CLI flags always override manifest settings. `infs run` ignores `[build] mode` entirely and always builds an executable in `out/` (proof-mode WASM contains non-deterministic opcodes that `wasmtime` cannot execute) — but it does honor `[build.wasm-opt]`, since `run` optimizes exactly what it then executes. `[build.wasm-opt]` applies only to compile-mode artifacts (proof-mode and `-v` builds always skip it) and can be skipped for a single invocation with `--no-wasm-opt`. `wasm-opt` itself does not need to be preinstalled: run `infs component add wasm-opt` to provision the pinned, checksum-verified Binaryen up front, or set `auto-install = true` under `[build.wasm-opt]` to have `infs` download it automatically the first time a build needs it. See [`docs/inference-toml.md`](docs/inference-toml.md) for the full field reference, including the non-deterministic-construct hard error and the complete `wasm-opt` resolution order.
 
 ### Run Command
 
@@ -139,9 +144,12 @@ infs run example.inf --entry-point helper
 
 # Pass arguments to the program (single-file only)
 infs run example.inf -- arg1 arg2
+
+# Project mode: build, but skip [build.wasm-opt] for this run
+infs run --no-wasm-opt
 ```
 
-Requires `wasmtime` to be installed.
+Requires `wasmtime` to be installed. In project mode, `infs run` applies the same `[build.wasm-opt]` post-build optimization as `infs build` before executing the result.
 
 ### Project Commands
 

apps/infs/docs/inference-toml.md

@@ -34,6 +34,11 @@ target = "wasm32"
 optimize = "debug"
 mode = "compile"    # "compile" (executable WASM) or "proof" (Rocq translation)
 
+[build.wasm-opt]        # optional: post-build optimization of the executable
+enabled = true          # table presence enables; set false to keep it off
+level = "3"             # forwarded as -O<level>: "0".."4", "s", "z"
+auto-install = false    # download wasm-opt automatically if it is missing
+
 [verification]
 output-dir = "proofs/"   # honored only in proof mode
 ```
@@ -130,6 +135,66 @@ optimize = "release"
 mode = "proof"
 ```
 
+### [build.wasm-opt]
+
+The `[build.wasm-opt]` table is an optional sub-table of `[build]` that enables post-build optimization of the compiled WASM executable via the external [Binaryen](https://github.com/WebAssembly/binaryen) `wasm-opt` binary. `infs` can provision `wasm-opt` for you — `infs component add wasm-opt` installs a pinned, checksum-verified Binaryen release, and `auto-install = true` does the same automatically at build time — or resolve one already on your system; resolution order is covered below.
+
+An `Inference.toml` with no `[build.wasm-opt]` table at all leaves the build pipeline unchanged — this feature is off by default.
+
+#### Fields
+
+- **`enabled`** (boolean, default: `true`): Whether the optimizer runs.
+  - Table *presence* is what turns the feature on: an empty `[build.wasm-opt]` table enables optimization at the default level. Set `enabled = false` to keep the table (and a configured `level`) in the manifest while disabling the step.
+
+- **`level`** (string, default: `"3"`): The optimization level, forwarded to `wasm-opt` as `-O<level>`.
+  - One of `"0"`, `"1"`, `"2"`, `"3"`, `"4"`, `"s"`, `"z"` — the same levels `wasm-opt` itself accepts (`s` and `z` bias toward size over speed). Any other value is a load error naming the offending value and the allowed set.
+
+- **`auto-install`** (boolean, default: `false`): Whether a missing `wasm-opt` is downloaded automatically at build time.
+  - When `true` and `wasm-opt` does not resolve in any of the three tiers below, `infs` downloads the pinned, sha256-verified Binaryen release into `~/.inference/tools/binaryen/<version>/` — the same install `infs component add wasm-opt` performs — before optimizing. The default `false` keeps a build network-free: a missing binary is a hard error with install remediation instead. The opt-in is recorded in the versioned manifest; `infs` has no interactive prompts.
+  - An invalid `WASM_OPT_PATH` override is always an error, even with `auto-install = true` — a typo in that variable is surfaced rather than silently downloaded over.
+
+#### Example
+
+```toml
+[build.wasm-opt]
+enabled = true
+level = "z"
+```
+
+#### When optimization runs
+
+- **Project mode only, for executable artifacts.** Both `infs build` and `infs run` apply `[build.wasm-opt]` to `out/main.wasm` after a successful compile — `run` optimizes exactly the artifact it then executes, so what you run is what `build` would have shipped. Single-file mode (`infs build file.inf`) never consults the manifest and is unaffected.
+- **Proof-mode and `-v` builds are always skipped, silently.** A build counts as proof mode when the effective `[build] mode` is `"proof"`, `--mode proof` is passed, or `-v` is passed at all (even without `--mode`). Their WASM can carry the non-deterministic opcodes (`forall`, `exists`, `assume`, `unique`, `@` uzumaki) that `wasm-opt` cannot parse, and they are a different artifact class from an executable.
+- **A compile-mode artifact that still contains a non-deterministic opcode is a hard error**, not a silent skip. Compile-mode builds strip `spec` blocks, so a well-formed executable should never carry one of these opcodes — if it does, `infs` scans for it before invoking `wasm-opt` (which would otherwise fail with an opaque parse error) and reports the offending construct by name, with remediation: move it into a `spec` block, or turn optimization off.
+
+#### Disabling optimization for one invocation
+
+Pass `--no-wasm-opt` to skip `[build.wasm-opt]` for a single `infs build` or `infs run` without editing the manifest:
+
+```bash
+infs build --no-wasm-opt
+infs run --no-wasm-opt
+```
+
+#### Resolving the `wasm-opt` binary
+
+`infs` resolves `wasm-opt` through three precedence tiers, in order:
+
+1. **`WASM_OPT_PATH`** environment variable, if set. It must point at an existing file, or the build errors naming the variable and the invalid path — a set override is never silently discarded in favor of a lower tier, even when `auto-install = true`.
+2. **PATH** — a standard lookup for `wasm-opt`. This tier wins over the managed tier below, so a system-installed `wasm-opt` on PATH always takes precedence over an infs-managed one.
+3. **Managed tools** — the pinned Binaryen installed by `infs component add wasm-opt` (or by `auto-install`, see below) at `~/.inference/tools/binaryen/<version>/`.
+
+Set `INFS_VERBOSE=1` to trace which tier resolved `wasm-opt` to stderr (`infs: resolved wasm-opt via <tier>: <path>`).
+
+If no tier resolves, the build fails with install hints led by `infs component add wasm-opt`, followed by the system package managers (`brew install binaryen`, `apt install binaryen`, `npm install -g binaryen`) and a link to the [Binaryen releases page](https://github.com/WebAssembly/binaryen/releases). Set `auto-install = true` to have `infs` provision Binaryen automatically at build time instead of erroring.
+
+The resolved binary must report **Binaryen 116 or newer** (`wasm-opt --version`); an older version is a hard error naming both the found and required versions. If `--version` cannot be run or its output cannot be parsed, `infs` warns and proceeds rather than blocking the build over an unrecognized binary. This check runs against whichever binary was resolved, managed installs included.
+
+#### Caveats
+
+- **Function names are dropped.** `wasm-opt` strips the WASM names custom section, so stack traces and any tooling that resolves function names from an optimized `out/main.wasm` will not see them. There is currently no flag to preserve it.
+- **Deterministic per Binaryen version, not across versions.** The same source, flags, and Binaryen version always produce identical optimized bytes, but upgrading Binaryen can change the output even for unchanged input. Do not treat an optimized `.wasm` as a stable byte-for-byte reference across toolchain upgrades.
+
 ### [verification]
 
 The `[verification]` section configures Rocq (Coq) proof generation.

apps/infs/src/commands/build.rs

@@ -67,7 +67,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::manifest::{InferenceToml, MANIFEST_FILE_NAME, find_manifest_dir};
 use crate::project::{self, ProjectContext};
 use crate::toolchain::find_infc;
 
@@ -118,6 +118,14 @@
     /// `use { … } from <module>;`. Repeatable; forwarded verbatim to `infc`.
     #[clap(short = 'L', long = "wasm-lib-dir", value_name = "DIR")]
     pub wasm_lib_dirs: Vec<PathBuf>,
+
+    /// Skip the `[build.wasm-opt]` post-build optimization for this build.
+    ///
+    /// Project mode only: when the manifest declares `[build.wasm-opt]`, this
+    /// leaves `out/main.wasm` exactly as `infc` emitted it. No effect in
+    /// single-file mode or when no `[build.wasm-opt]` table is present.
+    #[clap(long = "no-wasm-opt")]
+    pub no_wasm_opt: bool,
 }
 
 /// Executes the build command with the given arguments.
@@ -187,7 +195,8 @@
     }
 
     for (name, path) in manifest_wasm_dependencies(path)? {
-        cmd.arg("--wasm-dep").arg(format_wasm_dep_arg(&name, &path)?);
+        cmd.arg("--wasm-dep")
+            .arg(format_wasm_dep_arg(&name, &path)?);
     }
 
     let status = cmd
@@ -275,7 +284,13 @@
     let effective_mode = resolve_effective_mode(args.mode, &ctx.manifest.build.mode);
     let out_dir = resolve_out_dir(effective_mode, &ctx.manifest.verification)?;
 
-    run_project_build(ctx, args.generate_v_output, effective_mode, out_dir.as_deref())
+    run_project_build(
+        ctx,
+        args.generate_v_output,
+        effective_mode,
+        out_dir.as_deref(),
+        args.no_wasm_opt,
+    )
 }
 
 /// Resolves the effective `--mode` to forward to `infc`, or `None` to forward
@@ -383,7 +398,9 @@
         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")
+            .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();
@@ -449,7 +466,10 @@
 
     #[test]
     fn manifest_proof_forwards_proof() {
-        assert_eq!(resolve_effective_mode(None, "proof"), Some(BuildMode::Proof));
+        assert_eq!(
+            resolve_effective_mode(None, "proof"),
+            Some(BuildMode::Proof)
+        );
     }
 
     #[test]