From 00bdabad0bd2d6e2438b85ebc16f344ef422fd3a Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Thu, 23 Jul 2026 23:32:17 +0100
Subject: [PATCH 1/2] Fixes #130: Wire in codegen pipeline to ECHIDNA and
 property corpus

---
 Cargo.lock                        | 88 +++++++++++++------------------
 tests/echidna/echidna-harness.mjs | 61 ++++++++++++++++++++-
 tests/property/property_test.mjs  | 37 ++++++++++++-
 3 files changed, 134 insertions(+), 52 deletions(-)

diff --git a/Cargo.lock b/Cargo.lock
index 5cb6dc0..5d19eb4 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -4,15 +4,15 @@ version = 4
 
 [[package]]
 name = "anyhow"
-version = "1.0.103"
+version = "1.0.104"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2a4385e2e34eb35d6b3efe798b9eb88096925d87726c0798709bf56d9ed84af3"
+checksum = "330a5ed07fa54e4702c9d6c4174f74427fc0ef6e214bbd677ae50a5099946470"
 
 [[package]]
 name = "bitflags"
-version = "2.11.1"
+version = "2.13.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c4512299f36f043ab09a583e57bceb5a5aab7a73db1805848e8fef3c9e8c78b3"
+checksum = "b588b76d00fde79687d7646a9b5bdf3cc0f655e0bbd080335a95d7e96f3587da"
 
 [[package]]
 name = "bumpalo"
@@ -84,24 +84,24 @@ checksum = "b6d2cec3eae94f9f509c767b45932f1ada8350c4bdb85af2fcab4a3c14807981"
 
 [[package]]
 name = "memchr"
-version = "2.8.2"
+version = "2.8.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "88904434abc2901f197fe8cc55f0445e7ded921dba5911dad2e2b39b48e663c4"
+checksum = "cf8baf1c55e62ffcace7a9f06f4bd9cd3f0c4beb022d3b367256b91b87513d98"
 
 [[package]]
 name = "proc-macro2"
-version = "1.0.106"
+version = "1.0.107"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934"
+checksum = "985e7ec9bb745e6ce6535b544d84d6cd6f7ad8bd711c398938ae983b91a766d9"
 dependencies = [
  "unicode-ident",
 ]
 
 [[package]]
 name = "quote"
-version = "1.0.45"
+version = "1.0.47"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "41f2619966050689382d2b44f664f4bc593e129785a36d6ee376ddf37259b924"
+checksum = "1fbf4db142a473a8d80c26bbf18454ed458bf8d26c8219c331daecfdbd079001"
 dependencies = [
  "proc-macro2",
 ]
@@ -114,27 +114,27 @@ checksum = "8a7852d02fc848982e0c167ef163aaff9cd91dc640ba85e263cb1ce46fae51cd"
 
 [[package]]
 name = "serde"
-version = "1.0.228"
+version = "1.0.229"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9a8e94ea7f378bd32cbbd37198a4a91436180c5bb472411e48b5ec2e2124ae9e"
+checksum = "4148590afebada386688f18773da617792bf2ef03ffc1e4cbd2b1d45b023e0ba"
 dependencies = [
  "serde_core",
 ]
 
 [[package]]
 name = "serde_core"
-version = "1.0.228"
+version = "1.0.229"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "41d385c7d4ca58e59fc732af25c3983b67ac852c1a25000afe1175de458b67ad"
+checksum = "67dca2c9c51e58a4791a4b1ed58308b39c64224d349a935ab5039aa360942a48"
 dependencies = [
  "serde_derive",
 ]
 
 [[package]]
 name = "serde_derive"
-version = "1.0.228"
+version = "1.0.229"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d540f220d3187173da220f885ab66608367b6574e925011a9353e4badda91d79"
+checksum = "e7a5d71263a5a7d47b41f6b3f06ba276f10cc18b0931f1799f710578e2309348"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -143,9 +143,9 @@ dependencies = [
 
 [[package]]
 name = "spin"
-version = "0.9.8"
+version = "0.9.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6980e8d7511241f8acf4aebddbb1ff938df5eebe98691418c4468d0b72a96a67"
+checksum = "3763264f6b73151db08c50ff20d7d8a0b8796e021cdea7ceedad07b80155fa0e"
 
 [[package]]
 name = "string-interner"
@@ -159,9 +159,9 @@ dependencies = [
 
 [[package]]
 name = "syn"
-version = "2.0.117"
+version = "3.0.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e665b8803e7b1d2a727f4023456bbbbe74da67099c585258af0ad9c5013b9b99"
+checksum = "53e9bae58849f64dfa4f5d5ae372c8341f7305f82a3868709269343628b659a3"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -179,18 +179,18 @@ dependencies = [
 
 [[package]]
 name = "thiserror"
-version = "2.0.18"
+version = "2.0.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4288b5bcbc7920c07a1149a35cf9590a2aa808e0bc1eafaade0b80947865fbc4"
+checksum = "09a43598840e33d5b0331f38c5e30d13bb11c11210a4b58f0d9b18a5a5eefcd9"
 dependencies = [
  "thiserror-impl",
 ]
 
 [[package]]
 name = "thiserror-impl"
-version = "2.0.18"
+version = "2.0.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ebc4ee7f67670e9b64d05fa4253e753e016c6c95ff35b89b7941d6b856dec1d5"
+checksum = "43cbfe0cf76104d42a574802844187e84a305e531ed54455f11fbde0f10541cd"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -223,7 +223,7 @@ name = "typed-wasm-verify"
 version = "0.1.0"
 dependencies = [
  "thiserror",
- "wasm-encoder",
+ "wasm-encoder 0.253.0",
  "wasmparser 0.253.0",
 ]
 
@@ -241,22 +241,22 @@ checksum = "b4ac048d71ede7ee76d585517add45da530660ef4390e49b098733c6e897f254"
 
 [[package]]
 name = "wasm-encoder"
-version = "0.252.0"
+version = "0.253.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8185ae345fa5687c054626ff9a50e7089797a343d9904d1dc9820eb4c4d3196f"
+checksum = "59972d6cd272259de647b7c1f1912e45e289c75ffd4be04e10695507cd7e1b59"
 dependencies = [
  "leb128fmt",
- "wasmparser 0.252.0",
+ "wasmparser 0.253.0",
 ]
 
 [[package]]
 name = "wasm-encoder"
-version = "0.253.0"
+version = "0.254.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "59972d6cd272259de647b7c1f1912e45e289c75ffd4be04e10695507cd7e1b59"
+checksum = "09480d646178e5fdd12bb06e812d0af9a3a191dbc9cd697fdc86687beade7393"
 dependencies = [
  "leb128fmt",
- "wasmparser 0.253.0",
+ "wasmparser 0.254.0",
 ]
 
 [[package]]
@@ -310,17 +310,6 @@ dependencies = [
  "indexmap",
 ]
 
-[[package]]
-name = "wasmparser"
-version = "0.252.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d3eb099dcadcde5be9eef55e3a337128efd4e44b4c93122487e4d2e4e1c6627c"
-dependencies = [
- "bitflags",
- "indexmap",
- "semver",
-]
-
 [[package]]
 name = "wasmparser"
 version = "0.253.0"
@@ -336,13 +325,12 @@ dependencies = [
 
 [[package]]
 name = "wasmparser"
-version = "0.253.0"
+version = "0.254.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "19db11f87d2486580e1e8b6f494c54df7e0566b87d0b599db843c24019667339"
+checksum = "d5769a29f799fbab136aaf65b4fe5384cd7d93fe6fc9ba0dcb6c8382a1f16e27"
 dependencies = [
  "bitflags",
  "indexmap",
- "semver",
 ]
 
 [[package]]
@@ -358,22 +346,22 @@ dependencies = [
 
 [[package]]
 name = "wast"
-version = "252.0.0"
+version = "254.0.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "942a3449d6a593fccc111a6241c8df52bda168af30e40bf9580d4394d7374c65"
+checksum = "e7ed4dfc8f6b9fc38b231065e2cdfbf7359af5ab945990abf09658dcc63c3e32"
 dependencies = [
  "bumpalo",
  "leb128fmt",
  "memchr",
  "unicode-width",
- "wasm-encoder 0.252.0",
+ "wasm-encoder 0.254.0",
 ]
 
 [[package]]
 name = "wat"
-version = "1.252.0"
+version = "1.254.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c72a4ba7088f7bac94cf516e49882bdf97068904a563768cf249efc839ec42cb"
+checksum = "7127f7f9b8f127c879991cecd35f494e4628bae1b0874c681414d8d8831e952c"
 dependencies = [
  "wast",
 ]
diff --git a/tests/echidna/echidna-harness.mjs b/tests/echidna/echidna-harness.mjs
index 7ddb4a1..fcbdf7e 100644
--- a/tests/echidna/echidna-harness.mjs
+++ b/tests/echidna/echidna-harness.mjs
@@ -453,9 +453,10 @@ console.log(
 // provide ECHIDNA with proof-of-absence obligations that can be independently
 // verified.
 
-import { readFileSync as _readFileSync } from "node:fs";
+import { readFileSync as _readFileSync, writeFileSync as _writeFileSync, rmSync as _rmSync, existsSync as _existsSync } from "node:fs";
 import { resolve as _resolve } from "node:path";
 import { fileURLToPath as _fileURLToPath } from "node:url";
+import { execSync as _execSync } from "node:child_process";
 
 // _thisFile is the path to this harness file, not a directory.
 // The resolve chain strips the filename (first ..) then navigates to the layout dir.
@@ -556,6 +557,54 @@ console.log(recCheck.ok  ? "  ✓ Types.idr: WHT_Var, WHT_Rec, WHT_Any present"
 console.log(listCheck.ok ? "  ✓ Stdlib.idr: List uses WHT_Var 0 (no placeholder)"
                          : `  ✗ list-layout: ${listCheck.reason}`);
 
+// ============================================================================
+// Property 6: Fuzzing Round-Trip Soundness (verify(codegen(parse)))
+// ============================================================================
+console.log("\nProperty 6: Fuzzing Round-Trip Soundness");
+
+const TW_BIN = _resolve(_thisFile, "..", "..", "..", "target", "debug", "tw");
+const TW_VERIFY_BIN = _resolve(_thisFile, "..", "..", "..", "target", "debug", "tw-verify");
+
+let soundnessPass = 0;
+let soundnessFail = 0;
+let soundnessSkipped = 0;
+
+if (!_existsSync(TW_BIN) || !_existsSync(TW_VERIFY_BIN)) {
+  console.log("  SKIP: Codegen binaries not found. Run `cargo build` first.");
+  soundnessSkipped = Math.min(iterations, 50);
+} else {
+  const maxIterations = process.env.EXHAUSTIVE_FUZZ ? iterations : Math.min(iterations, 50);
+  if (!process.env.EXHAUSTIVE_FUZZ && iterations > 50) {
+    console.log(`  (Capping codegen fuzzing to 50 iterations. Set EXHAUSTIVE_FUZZ=1 for all ${iterations})`);
+  }
+  
+  for (let i = 0; i < maxIterations; i++) {
+    const rng = new RNG(i + 50000);
+    const prog = genProgram(rng);
+    const result = parseModule(prog);
+
+    if (result.TAG === "Ok") {
+      property(`round-trip soundness seed=${i}`, () => {
+        const tempSrc = _resolve(_thisFile, "..", `temp_${i}.twasm`);
+        const tempWasm = _resolve(_thisFile, "..", `temp_${i}.wasm`);
+        try {
+          _writeFileSync(tempSrc, prog);
+          _execSync(`${TW_BIN} build ${tempSrc} -o ${tempWasm}`, { stdio: 'pipe' });
+          _execSync(`${TW_VERIFY_BIN} ${tempWasm}`, { stdio: 'pipe' });
+          soundnessPass++;
+        } catch (e) {
+          soundnessFail++;
+          const stderr = e.stderr ? e.stderr.toString() : e.message;
+          throw new Error(`Codegen or verify failed: ${stderr}`);
+        } finally {
+          try { _rmSync(tempSrc); } catch {}
+          try { _rmSync(tempWasm); } catch {}
+        }
+      });
+    }
+  }
+}
+
 // ============================================================================
 // ECHIDNA Submission
 // ============================================================================
@@ -624,6 +673,16 @@ try {
               `unchanged modulo proof-only keys (effects, caps, loc) in ` +
               `${erasureMatched}/${erasurePairs} successful pairs.`,
         },
+        {
+          name: "fuzz-round-trip-soundness",
+          status: soundnessSkipped > 0 ? "info" : (soundnessFail === 0 && soundnessPass > 0 ? "proved" : "failed"),
+          successes: soundnessPass,
+          failures: soundnessFail,
+          skipped: soundnessSkipped,
+          detail: soundnessSkipped > 0 
+            ? "Skipped due to missing codegen binaries" 
+            : `${soundnessPass} passed, ${soundnessFail} failed round-trip`,
+        },
       ],
     }),
   });
diff --git a/tests/property/property_test.mjs b/tests/property/property_test.mjs
index d857a42..dd9ede3 100644
--- a/tests/property/property_test.mjs
+++ b/tests/property/property_test.mjs
@@ -25,7 +25,8 @@
 //
 // Run:  node tests/property/property_test.mjs
 
-import { readFileSync, readdirSync, existsSync, statSync } from "node:fs";
+import { readFileSync, readdirSync, existsSync, statSync, mkdirSync, copyFileSync } from "node:fs";
+import { execSync } from "node:child_process";
 import { resolve, dirname, join } from "node:path";
 import { fileURLToPath } from "node:url";
 
@@ -229,6 +230,40 @@ for (const path of EXAMPLES.slice(0, 3)) {
   }
 }
 
+// ----------------------------------------------------------------------
+// P9  Round-trip soundness (verify(codegen(parse(src))) == OK)
+// ----------------------------------------------------------------------
+section("P9. Round-trip soundness (verify(codegen(parse(src))) == OK)");
+
+const TW_BIN = join(ROOT, "target/debug/tw");
+const TW_VERIFY_BIN = join(ROOT, "target/debug/tw-verify");
+const FIXTURES_DIR = join(ROOT, "crates/typed-wasm-verify/tests/fixtures/c5_real");
+
+if (!existsSync(TW_BIN) || !existsSync(TW_VERIFY_BIN)) {
+  skip("P9: Codegen binaries not found (run `cargo build` first)");
+} else {
+  mkdirSync(FIXTURES_DIR, { recursive: true });
+  for (const path of EXAMPLES) {
+    const filename = path.split("/").pop();
+    const tempWasm = join(ROOT, `temp_${filename}.wasm`);
+    const fixturePath = join(FIXTURES_DIR, `${filename.replace(".twasm", ".wasm")}`);
+
+    try {
+      execSync(`${TW_BIN} build ${path} -o ${tempWasm}`, { stdio: 'pipe' });
+      execSync(`${TW_VERIFY_BIN} ${tempWasm}`, { stdio: 'pipe' });
+      copyFileSync(tempWasm, fixturePath);
+      ok(`${path}: verify(codegen) == OK`);
+    } catch (e) {
+      const stderr = e.stderr ? e.stderr.toString() : e.message;
+      bad(`${path}: codegen or verify failed:\n${stderr}`);
+    } finally {
+      if (existsSync(tempWasm)) {
+        try { import("node:fs").then(fs => fs.rmSync(tempWasm)); } catch {}
+      }
+    }
+  }
+}
+
 // ----------------------------------------------------------------------
 // Summary
 // ----------------------------------------------------------------------

From 33e45831623f01daca45370aff87dd75a3e68e3f Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Thu, 23 Jul 2026 23:56:57 +0100
Subject: [PATCH 2/2] test: use execFileSync instead of execSync to mitigate
 command injection (GHAS)

---
 tests/property/property_test.mjs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tests/property/property_test.mjs b/tests/property/property_test.mjs
index dd9ede3..79977f9 100644
--- a/tests/property/property_test.mjs
+++ b/tests/property/property_test.mjs
@@ -26,7 +26,7 @@
 // Run:  node tests/property/property_test.mjs
 
 import { readFileSync, readdirSync, existsSync, statSync, mkdirSync, copyFileSync } from "node:fs";
-import { execSync } from "node:child_process";
+import { execFileSync } from "node:child_process";
 import { resolve, dirname, join } from "node:path";
 import { fileURLToPath } from "node:url";
 
@@ -249,8 +249,8 @@ if (!existsSync(TW_BIN) || !existsSync(TW_VERIFY_BIN)) {
     const fixturePath = join(FIXTURES_DIR, `${filename.replace(".twasm", ".wasm")}`);
 
     try {
-      execSync(`${TW_BIN} build ${path} -o ${tempWasm}`, { stdio: 'pipe' });
-      execSync(`${TW_VERIFY_BIN} ${tempWasm}`, { stdio: 'pipe' });
+      execFileSync(TW_BIN, ['build', path, '-o', tempWasm], { stdio: 'pipe' });
+      execFileSync(TW_VERIFY_BIN, [tempWasm], { stdio: 'pipe' });
       copyFileSync(tempWasm, fixturePath);
       ok(`${path}: verify(codegen) == OK`);
     } catch (e) {