SPIN verification (PoC)

MODULE.bazel

@@ -140,6 +140,10 @@ use_repo(perfetto_ext, "perfetto_cfg")
 # Perfetto requires this to get through bazel analysis, but seems unused for our use.
 bazel_dep(name = "rules_android", version = "0.6.0")
 
+# SPIN model checker — used by xls/spin to verify Promela models generated from XLS IR.
+spin_ext = use_extension("//dependency_support/spin:extension.bzl", "spin_extension")
+use_repo(spin_ext, "spin")
+
 # Pin this as otherwise we encounter some bazel analysis failure.
 bazel_dep(name = "rules_jvm_external", version = "6.8")
 

dependency_support/spin/BUILD.bazel

@@ -0,0 +1,17 @@
+# Copyright 2026 The XLS Authors
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#      http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+# Support files for the SPIN model-checker dependency.
+
+exports_files(["bundled.BUILD.bazel"])

dependency_support/spin/bundled.BUILD.bazel

@@ -0,0 +1,94 @@
+# Copyright 2026 The XLS Authors
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#      http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+# Build rules for the SPIN model checker.
+# https://spinroot.com / https://github.com/nimble-code/Spin
+
+load("@rules_cc//cc:defs.bzl", "cc_binary")
+
+licenses(["notice"])  # BSD-like, see Src/LICENSE
+
+exports_files(["Src/LICENSE"])
+
+package(default_visibility = ["//visibility:public"])
+
+# Process spin.y with bison; produces y.tab.c and y.tab.h.
+genrule(
+    name = "spin_yacc_gen",
+    srcs = ["Src/spin.y"],
+    outs = [
+        "y.tab.c",
+        "y.tab.h",
+    ],
+    cmd = "M4=$(M4) $(BISON) --yacc --defines=$(location y.tab.h) -o $(location y.tab.c) $(location Src/spin.y) 2>/dev/null",
+    toolchains = [
+        "@rules_bison//bison:current_bison_toolchain",
+        "@rules_m4//m4:current_m4_toolchain",
+    ],
+    visibility = ["//visibility:private"],
+)
+
+cc_binary(
+    name = "spin",
+    srcs = [
+        "Src/dstep.c",
+        "Src/flow.c",
+        "Src/guided.c",
+        "Src/main.c",
+        "Src/mesg.c",
+        "Src/msc_tcl.c",
+        "Src/pangen1.c",
+        "Src/pangen1.h",
+        "Src/pangen2.c",
+        "Src/pangen2.h",
+        "Src/pangen3.c",
+        "Src/pangen3.h",
+        "Src/pangen4.c",
+        "Src/pangen4.h",
+        "Src/pangen5.c",
+        "Src/pangen5.h",
+        "Src/pangen6.c",
+        "Src/pangen6.h",
+        "Src/pangen7.c",
+        "Src/pangen7.h",
+        "Src/reprosrc.c",
+        "Src/run.c",
+        "Src/sched.c",
+        "Src/spin.h",
+        "Src/spinlex.c",
+        "Src/structs.c",
+        "Src/sym.c",
+        "Src/tl.h",
+        "Src/tl_buchi.c",
+        "Src/tl_cache.c",
+        "Src/tl_lex.c",
+        "Src/tl_main.c",
+        "Src/tl_mem.c",
+        "Src/tl_parse.c",
+        "Src/tl_rewrt.c",
+        "Src/tl_trans.c",
+        "Src/vars.c",
+        "Src/version.h",
+        ":spin_yacc_gen",
+    ],
+    copts = [
+        "-O2",
+        "-DNXT",
+        "-w",
+    ],
+    includes = [
+        ".",
+        "Src",
+    ],
+)

dependency_support/spin/extension.bzl

@@ -0,0 +1,39 @@
+# Copyright 2026 The XLS Authors
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#      http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+"""Module extension for the SPIN model checker (https://spinroot.com)."""
+
+load("@bazel_tools//tools/build_defs/repo:http.bzl", "http_archive")
+
+def _spin_extension_impl(_ctx):
+    http_archive(
+        name = "spin",
+        sha256 = "e2ba8cfebf963cb524be2a3caee68821472602f9c4f0e557f2550d8e382eab99",
+        strip_prefix = "Spin-master",
+        urls = ["https://github.com/nimble-code/Spin/archive/refs/heads/master.tar.gz"],
+        build_file = Label("//dependency_support/spin:bundled.BUILD.bazel"),
+        patches = [
+            # Adds -Q <file>: emits one JSON line per channel event during
+            # simulation, used by xls/spin/ to verify equivalence of channel
+            # communication between the Promela model and the DSLX source proc.
+            # SPIN has no built-in machine-readable channel output.
+            Label("//dependency_support/spin/patches:spin_json_trace.patch"),
+            # Adds -K<dir>: pan writes .trail files into <dir> instead of cwd.
+            # Adds -H: pan exits with code 1 when errors > 0 (default is 0).
+            Label("//dependency_support/spin/patches:spin_trail_and_exit.patch"),
+        ],
+        patch_args = ["-p1", "--fuzz=3"],
+    )
+
+spin_extension = module_extension(implementation = _spin_extension_impl)

dependency_support/spin/patches/BUILD.bazel

@@ -0,0 +1,15 @@
+# Copyright 2026 The XLS Authors
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#      http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+exports_files(["spin_json_trace.patch"])