refactor: carve verification core into wsc-verify-core (wasm-buildable)

.github/workflows/formal-verification.yml

@@ -63,9 +63,13 @@ jobs:
       matrix:
         include:
           - module: varint
+            # `wasm_module::varint` lives in `wsc-verify-core` after the
+            # carve, so the harness must be invoked against that crate.
+            pkg: wsc-verify-core
             harness: wasm_module::varint
             tolerate_failure: false
           - module: merkle
+            pkg: wsc
             harness: signature::keyless::merkle
             # WIP — see audit C-7 partial closure. Three of the five harnesses
             # in this module call SHA-256 with symbolic input; the sha2 crate's
@@ -76,6 +80,7 @@ jobs:
             # the scope of bounded model checking entirely.
             tolerate_failure: true
           - module: dsse
+            pkg: wsc
             harness: dsse
             # WIP — CI observation post-rebase: dsse harnesses also hit
             # "unwinding assertion loop 0" at --default-unwind 4. The
@@ -85,6 +90,7 @@ jobs:
             # loop inside the prefix comparison.
             tolerate_failure: true
           - module: format
+            pkg: wsc
             harness: format
             # WIP — see audit C-7 partial closure. CI observation: the format
             # harnesses fail under cargo kani --default-unwind 4 despite static
@@ -96,17 +102,20 @@ jobs:
             # harness rather than enumerating in one 4-byte-symbolic harness.
             tolerate_failure: true
           - module: wasm_module
-            # Filter was wasm_module::tests, which matched no harness (the
-            # module is named component_proofs, not tests). Fixed in this PR
-            # so the single harness — header mutual-exclusivity — actually
-            # runs. CI observation: the harness hits an unwinding-loop
-            # assertion inside <builtin-library-memcmp> at the default
-            # unwind of 4. Static analysis missed this; the harness's
-            # equality check on the 8-byte header lowers to memcmp at the
-            # MIR level. Needs a per-harness #[kani::unwind(9)] (or
-            # rewriting the equality as a per-byte comparison) before this
-            # can be unmasked. Filter-fix lands here; harness-fix is a
-            # follow-up.
+            # `wasm_module::component_proofs` lives in `wsc-verify-core`
+            # after the carve, so the harness must be invoked against that
+            # crate. Filter was wasm_module::tests, which matched no
+            # harness (the module is named component_proofs, not tests).
+            # Fixed in this PR so the single harness — header mutual-
+            # exclusivity — actually runs. CI observation: the harness
+            # hits an unwinding-loop assertion inside <builtin-library-
+            # memcmp> at the default unwind of 4. Static analysis missed
+            # this; the harness's equality check on the 8-byte header
+            # lowers to memcmp at the MIR level. Needs a per-harness
+            # #[kani::unwind(9)] (or rewriting the equality as a per-byte
+            # comparison) before this can be unmasked. Filter-fix lands
+            # here; harness-fix is a follow-up.
+            pkg: wsc-verify-core
             harness: wasm_module::component_proofs
             tolerate_failure: true
     steps:
@@ -129,7 +138,8 @@ jobs:
     - name: Run Kani ${{ matrix.module }} proofs
       env:
         HARNESS: ${{ matrix.harness }}
-      run: cargo kani -p wsc --default-unwind 4 --output-format terse --harness "$HARNESS"
+        PACKAGE: ${{ matrix.pkg }}
+      run: cargo kani -p "$PACKAGE" --default-unwind 4 --output-format terse --harness "$HARNESS"
       timeout-minutes: 60
       continue-on-error: ${{ matrix.tolerate_failure }}
 

.github/workflows/supply-chain.yml

@@ -92,30 +92,54 @@ jobs:
         tool: cargo-mutants
     - name: Run mutation testing on security-critical modules
       run: |
-        cargo mutants -p wsc --timeout 120 --jobs 4 --output mutants-out \
+        cargo mutants -p wsc --timeout 120 --jobs 4 --output mutants-wsc \
           -f src/lib/src/signature/ \
           -f src/lib/src/dsse.rs \
           -f src/lib/src/format/ \
           -E "proofs::" \
           -E "key_id" \
           -- --lib
+    # The classic verification core lives in `wsc-verify-core` after the
+    # carve. Running cargo-mutants on it too keeps the zero-survivor gate
+    # on the moved signature code — without this step the original `-f
+    # src/lib/src/signature/` filter would silently match almost nothing
+    # post-merge and the gate would pass for the wrong reason.
+    - name: Run mutation testing on wsc-verify-core (carved verification core)
+      run: |
+        cargo mutants -p wsc-verify-core --timeout 120 --jobs 4 \
+          --output mutants-verify-core \
+          -f src/verify-core/src/signature/ \
+          -E "proofs::" \
+          -- --lib
     - name: Check surviving mutants
       run: |
-        if [ -f mutants-out/missed.txt ]; then
-          MISSED=$(wc -l < mutants-out/missed.txt | tr -d ' ')
-        else
-          MISSED=0
-        fi
-        echo "Surviving mutants: $MISSED"
-        if [ "$MISSED" -gt 0 ]; then
-          echo "::error::$MISSED mutant(s) survived — tests must catch all mutations in security-critical code"
-          cat mutants-out/missed.txt | head -30
+        missed_count() {
+          if [ -f "$1/missed.txt" ]; then
+            wc -l < "$1/missed.txt" | tr -d ' '
+          else
+            echo 0
+          fi
+        }
+        WSC=$(missed_count mutants-wsc)
+        CORE=$(missed_count mutants-verify-core)
+        TOTAL=$((WSC + CORE))
+        echo "Surviving mutants: wsc=$WSC, wsc-verify-core=$CORE, total=$TOTAL"
+        if [ "$TOTAL" -gt 0 ]; then
+          echo "::error::$TOTAL mutant(s) survived — tests must catch all mutations in security-critical code"
+          for d in mutants-wsc mutants-verify-core; do
+            if [ -f "$d/missed.txt" ]; then
+              echo "--- $d/missed.txt ---"
+              head -15 "$d/missed.txt"
+            fi
+          done
           exit 1
         fi
         echo "All mutants killed!"
-    - name: Upload mutants report
+    - name: Upload mutants reports
       if: always()
       uses: actions/upload-artifact@v4
       with:
-        name: mutants-report
-        path: mutants-out/
+        name: mutants-reports
+        path: |
+          mutants-wsc/
+          mutants-verify-core/

Cargo.toml

@@ -3,11 +3,13 @@ resolver = "2"
 members = [
     "src/attestation",
     "src/cli",
-    "src/lib",
     "src/component",
+    "src/lib",
+    "src/verify-core",
 ]
 exclude = [
     "examples/wasmtime-loader",
+    "verification/witness-harness",
 ]
 
 [workspace.package]

src/component/src/lib.rs

@@ -88,11 +88,15 @@ impl Guest for Component {
         // Create a reader over the module bytes
         let mut reader = Cursor::new(&module_bytes);
 
-        // Verify based on signature type
+        // Verify based on signature type. `pk.verify` now returns
+        // `CoreError` (the carved verify-core error type), so the match
+        // patterns are `CoreError` variants — `From<CoreError> for WSError`
+        // handles `?` propagation in the rest of `wsc`, but a direct match
+        // here must be against the actual return type.
         match pk.verify(&mut reader, detached_sig.as_deref()) {
             Ok(()) => Ok(true),
-            Err(wsc::WSError::NoSignatures) => Ok(false),
-            Err(wsc::WSError::VerificationFailed) => Ok(false),
+            Err(wsc::CoreError::NoSignatures) => Ok(false),
+            Err(wsc::CoreError::VerificationFailed) => Ok(false),
             Err(e) => Err(format!("Verification error: {}", e)),
         }
     }

src/lib/BUILD.bazel

@@ -23,6 +23,7 @@ rust_library(
     ],
     deps = [
         "//src/attestation:wsc-attestation",
+        "//src/verify-core:wsc-verify-core",
         "@wsc_deps//:anyhow",
         "@wsc_deps//:ct-codecs",
         "@wsc_deps//:ed25519-compact",

src/lib/Cargo.toml

@@ -12,6 +12,9 @@ homepage = "https://github.com/pulseengine/wsc"
 categories = ["cryptography", "wasm"]
 
 [dependencies]
+# Verification core (carved out so it builds for wasm32 with no TLS/X.509 deps).
+# wsc re-exports its public API for backwards compatibility.
+wsc-verify-core = { version = "0.9.0", path = "../verify-core" }
 # Re-export attestation types from minimal crate
 wsc-attestation = { version = "0.9.0", path = "../attestation" }
 anyhow = "1.0.100"

src/lib/src/error.rs

@@ -166,6 +166,37 @@ impl From<x509_parser::error::X509Error> for WSError {
     }
 }
 
+// Lift errors from the verification core (`wsc-verify-core`) into `WSError`
+// so call sites in this crate can keep using `?` through the carve boundary
+// without manual mapping.
+impl From<wsc_verify_core::CoreError> for WSError {
+    fn from(err: wsc_verify_core::CoreError) -> Self {
+        use wsc_verify_core::CoreError as C;
+        match err {
+            C::InternalError(s) => WSError::InternalError(s),
+            C::ParseError => WSError::ParseError,
+            C::IOError(e) => WSError::IOError(e),
+            C::Eof => WSError::Eof,
+            C::UTF8Error(e) => WSError::UTF8Error(e),
+            C::CryptoError(e) => WSError::CryptoError(e),
+            C::UnsupportedModuleType => WSError::UnsupportedModuleType,
+            C::VerificationFailed => WSError::VerificationFailed,
+            C::VerificationFailedForPredicates => WSError::VerificationFailedForPredicates,
+            C::NoSignatures => WSError::NoSignatures,
+            C::UnsupportedKeyType => WSError::UnsupportedKeyType,
+            C::IncompatibleSignatureVersion => WSError::IncompatibleSignatureVersion,
+            C::DuplicateSignature => WSError::DuplicateSignature,
+            C::SignatureAlreadyAttached => WSError::SignatureAlreadyAttached,
+            C::DuplicatePublicKey => WSError::DuplicatePublicKey,
+            C::UnknownPublicKey => WSError::UnknownPublicKey,
+            C::TooManyHashes(n) => WSError::TooManyHashes(n),
+            C::TooManySignatures(n) => WSError::TooManySignatures(n),
+            C::TooManyCertificates(n) => WSError::TooManyCertificates(n),
+            C::TooManySections(n) => WSError::TooManySections(n),
+        }
+    }
+}
+
 // WASI HTTP error conversion for wasm32-wasip2 target
 #[cfg(all(target_arch = "wasm32", target_os = "wasi"))]
 impl From<wasi::http::types::ErrorCode> for WSError {