Add typed-wasm contractile invariants and k9 guard

Author: hyperpolymath

contractiles/k9/typed-wasm-guard.k9.ncl

@@ -0,0 +1,57 @@
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# K9 Validator: Typed Wasm Guard
+# Ensures the Typed Wasm project keeps its memory-safety contracts and parser invariants intact.
+
+let typed_wasm_guard = {
+  name = "typed-wasm-guard",
+  version = "1.0.0",
+  description = "Validates the core invariants for Typed Wasm (multi-module safety, lifetime tracking, parser integrity, and no template placeholders).",
+
+  checks = {
+    multi_module = {
+      description = "The Idris2 MultiModule proof exists in the ABI folder.",
+      severity = "error",
+      check_type = "file-exists",
+      file = "src/abi/TypedWasm/ABI/MultiModule.idr",
+    },
+
+    lifetime_proof = {
+      description = "The Lifetime proof provides region-lifetime semantics.",
+      severity = "error",
+      check_type = "file-exists",
+      file = "src/abi/TypedWasm/ABI/Lifetime.idr",
+    },
+
+    levels_semantics = {
+      description = "The Levels semantics file is present for the 10-level lattice.",
+      severity = "warning",
+      check_type = "file-exists",
+      file = "src/abi/TypedWasm/ABI/Levels.idr",
+    },
+
+    parser_integrity = {
+      description = "The ReScript parser definition is included.",
+      severity = "error",
+      check_type = "file-exists",
+      file = "src/parser/Parser.res",
+    },
+
+    no_template_placeholders = {
+      description = "No {{PROJECT}}/ {{PLACEHOLDER}} tokens remain in the source base.",
+      severity = "error",
+      check_type = "file-pattern-guard",
+      scope = ".",
+      reject_patterns = ["{{PROJECT}}", "{{PLACEHOLDER}}", "rsr-template-repo"],
+    },
+
+    placeholder_fuzz_absent = {
+      description = "The placeholder fuzz file must not exist—it gives false security.",
+      severity = "warning",
+      check_type = "file-not-exists",
+      file = "tests/fuzz/placeholder.txt",
+    },
+  },
+}
+in typed_wasm_guard

contractiles/must/Mustfile.a2ml

@@ -40,3 +40,35 @@ that MUST hold at all times.
 - description: No Makefiles (use Justfile)
 - run: test ! -f Makefile
 - severity: warning
+
+## Invariants
+
+### multi-module-proof
+- description: Multi-module ABI proof file is present and tracked.
+- run: test -f src/abi/TypedWasm/ABI/MultiModule.idr
+- severity: critical
+
+### lifetime-proof
+- description: Lifetime semantics capture region safety for the proof domain.
+- run: test -f src/abi/TypedWasm/ABI/Lifetime.idr
+- severity: critical
+
+### levels-definition
+- description: The 10-level lattice file exists for type safety claims.
+- run: test -f src/abi/TypedWasm/ABI/Levels.idr
+- severity: warning
+
+### parser-definition
+- description: The ReScript parser definition is available.
+- run: test -f src/parser/Parser.res
+- severity: critical
+
+### no-template-placeholders
+- description: Replace template placeholders before publication.
+- run: "! rg '{{PROJECT}}\\|{{PLACEHOLDER}}\\|rsr-template-repo' -n src -g'*.*' 2>/dev/null | head -1 | grep -q ."
+- severity: error
+
+### placeholder-fuzz
+- description: Remove the placeholder fuzz file to avoid false coverage.
+- run: test ! -f tests/fuzz/placeholder.txt
+- severity: warning