chore: refresh #167 (rayon-wasm32) + #170 (rocq-gating doc) onto current main

.github/workflows/ci.yml

@@ -363,6 +363,15 @@ jobs:
     # Stays on ubuntu-latest: requires Nix + Bazel; both are out-of-scope for
     # smithy phase 1 (see migration playbook "What's currently out of scope").
     runs-on: ubuntu-latest
+    # continue-on-error is TEMPORARY, not the intended end state (loom#169).
+    # The job is currently red on the upstream rules_rocq_rust toolchain
+    # breakage (fix in flight: #141). Making it gating while red would block
+    # every merge. Plan to close loom#169:
+    #   1. land the rules_rocq_rust bump (#141) so this job goes green;
+    #   2. then REMOVE continue-on-error so a proof regression blocks merge;
+    #   3. separately discharge the proofs' remaining Admitted/Axiom (criterion
+    #      3 "complete") — gating catches regressions in the proven parts but
+    #      does not by itself close those gaps.
     continue-on-error: true
     steps:
       - uses: actions/checkout@v6

loom-core/Cargo.toml

@@ -32,6 +32,11 @@ leb128 = "0.2"
 # Parallel island-model optimization (v1.0.4 PR-islands, issue #71).
 # Scoped to loom-core only — the dependency boundary stays tight; CLI does
 # not depend on rayon, it just dispatches into the per-island entry point.
+# Excluded on wasm32: rayon's thread pool needs pthread, which the
+# single-threaded wasm32-wasip2 target can't link (#142). islands.rs falls
+# back to a sequential run there; the deterministic tie-break keeps it
+# bit-identical.
+[target.'cfg(not(target_arch = "wasm32"))'.dependencies]
 rayon = "1"
 
 [dev-dependencies]

loom-core/src/islands.rs

@@ -38,6 +38,9 @@
 
 use crate::Module;
 use anyhow::{Result, anyhow};
+// rayon is excluded on wasm32 (no pthread); islands run sequentially there.
+// The deterministic tie-break (see below) makes the result identical. (#142)
+#[cfg(not(target_arch = "wasm32"))]
 use rayon::prelude::*;
 
 /// Configuration for a single optimization island.
@@ -284,10 +287,18 @@ pub fn optimize_module_islands(module: &Module, configs: &[IslandConfig]) -> Res
     // `par_iter()` here yields `Result<IslandResult>`; we keep both Ok and
     // Err so we can preserve per-island failure messages for the no-winner
     // case below.
+    #[cfg(not(target_arch = "wasm32"))]
     let results: Vec<Result<IslandResult>> = configs
         .par_iter()
         .map(|cfg| run_one_island(module, cfg))
         .collect();
+    // wasm32 has no thread pool — run the same islands sequentially. The
+    // deterministic tie-break below makes the winner identical. (#142)
+    #[cfg(target_arch = "wasm32")]
+    let results: Vec<Result<IslandResult>> = configs
+        .iter()
+        .map(|cfg| run_one_island(module, cfg))
+        .collect();
 
     // Filter: keep only islands whose encoded output passes wasmparser
     // validation. This is defense-in-depth against the (rare) case where an
@@ -356,14 +367,25 @@ pub fn measure_island_sizes(
     module: &Module,
     configs: &[IslandConfig],
 ) -> Vec<(String, Result<usize>)> {
-    configs
+    #[cfg(not(target_arch = "wasm32"))]
+    let out = configs
         .par_iter()
         .map(|cfg| {
             let name = cfg.name.to_string();
             let result = run_one_island(module, cfg).map(|r| r.encoded.len());
             (name, result)
         })
-        .collect()
+        .collect();
+    #[cfg(target_arch = "wasm32")]
+    let out = configs
+        .iter()
+        .map(|cfg| {
+            let name = cfg.name.to_string();
+            let result = run_one_island(module, cfg).map(|r| r.encoded.len());
+            (name, result)
+        })
+        .collect();
+    out
 }
 
 #[cfg(test)]