From ecc8c72be4ea272e1e42a6b24cf3717e10c32376 Mon Sep 17 00:00:00 2001
From: SSD DDD <ssdm4@MacBook-Pro.local>
Date: Sat, 8 Aug 2026 00:20:01 +0700
Subject: [PATCH] ci(gft): execute GF-T spec test blocks under Icarus Verilog

New gft-verilog-kat workflow: t27c icarus-simulate generates a
self-checking testbench from tri_gft_add / tri_gft_sub / tri_gft_ladder and
runs it under iverilog -- the same specs that drive the Rust verifier and
the synthesizable silicon now have their assertions executed on the Verilog
path in CI. Requires t27c >= gHashTag/t27#1885 (assert lowering).
tri_gft_arith stays out until the upstream u64 width bug (t27#1886) is
fixed.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 .github/workflows/gft-verilog-kat.yml | 63 +++++++++++++++++++++++++++
 1 file changed, 63 insertions(+)
 create mode 100644 .github/workflows/gft-verilog-kat.yml

diff --git a/.github/workflows/gft-verilog-kat.yml b/.github/workflows/gft-verilog-kat.yml
new file mode 100644
index 00000000..8d3b76ff
--- /dev/null
+++ b/.github/workflows/gft-verilog-kat.yml
@@ -0,0 +1,63 @@
+name: gft-verilog-kat
+on:
+  push:
+    branches: [main]
+  pull_request:
+    paths:
+      - "specs/tri_gft_add.t27"
+      - "specs/tri_gft_sub.t27"
+      - "specs/tri_gft_ladder.t27"
+      - ".github/workflows/gft-verilog-kat.yml"
+
+# Execute the GF-T specs' own test blocks IN SIMULATED HARDWARE: t27c
+# icarus-simulate generates a self-checking Verilog testbench from the spec
+# and runs it under Icarus Verilog. This is the gen-verilog leg of the ring's
+# verification -- the same spec that drives the Rust verifier and the
+# synthesizable silicon now has its assertions executed on the Verilog path
+# too, so a codegen or spec regression on the hardware side cannot land
+# silently. Requires t27c >= gHashTag/t27#1885 (assert lowering).
+#
+# tri_gft_arith is EXCLUDED: its GF-T32 u64-helper tests fail in simulation
+# due to a pre-existing u64 width-truncation bug in gen-verilog
+# (gHashTag/t27#1886); add it back when that is fixed upstream.
+
+jobs:
+  icarus-kat:
+    name: GF-T spec KATs under Icarus Verilog
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout tri-net
+        uses: actions/checkout@v4
+        with:
+          path: tri-net
+
+      - name: Checkout t27 (SSOT compiler source)
+        uses: actions/checkout@v4
+        with:
+          repository: gHashTag/t27
+          ref: master
+          path: t27
+
+      - name: Install Icarus Verilog
+        run: sudo apt-get update && sudo apt-get install -y iverilog
+
+      - name: Install stable Rust toolchain
+        uses: dtolnay/rust-toolchain@stable
+
+      - name: Build t27c (release)
+        working-directory: t27
+        run: cargo build --release --manifest-path bootstrap/Cargo.toml --bin t27c
+
+      - name: Simulate GF-T spec testbenches
+        working-directory: tri-net
+        run: |
+          T27C=../t27/target/release/t27c
+          STATUS=0
+          for spec in tri_gft_add tri_gft_sub tri_gft_ladder; do
+            echo "== ${spec}"
+            if ! $T27C icarus-simulate specs/${spec}.t27; then
+              echo "::error file=specs/${spec}.t27::icarus-simulate failed for specs/${spec}.t27"
+              STATUS=1
+            fi
+          done
+          exit $STATUS