ci(fpga): the vacuous greens are gates again

.github/workflows/fpga-build.yml

@@ -163,7 +163,11 @@ jobs:
           total=$((pass+fail))
           echo "**Result:** $pass/$total modules passed Yosys lint" >> $GITHUB_STEP_SUMMARY
           if [ "$fail" -gt 0 ]; then
-            echo "::warning::$fail/$total modules failed Yosys lint"
+            # Audit 2026-08-19: a warning-only gate absorbed a live codegen
+            # regression (fifo.v invalid Verilog) within 40 minutes of the
+            # 32/32 claim. Lint failures now fail the step.
+            echo "::error::$fail/$total modules failed Yosys lint"
+            exit 1
           fi
 
   fpga-synthesis:
@@ -522,7 +526,6 @@ jobs:
     timeout-minutes: 45
     needs: fpga-smoke
     runs-on: ubuntu-latest
-    continue-on-error: true
     steps:
       - uses: actions/checkout@v6
 
@@ -578,6 +581,9 @@ jobs:
           echo "" >> $GITHUB_STEP_SUMMARY
           echo "| Module | Solver | Task | Result |" >> $GITHUB_STEP_SUMMARY
           echo "|--------|--------|------|--------|" >> $GITHUB_STEP_SUMMARY
+          # Audit 2026-08-19: without pipefail the if tested tee's exit (always 0),
+          # so PASS was recorded unconditionally and the FAIL branch was unreachable.
+          set -o pipefail
           if command -v sby &>/dev/null; then
             cp -r contrib/formal build/fpga/formal
             cp specs/fpga/mac.v build/fpga/formal/ 2>/dev/null || cp build/fpga/generated/mac.v build/fpga/formal/ 2>/dev/null || true
@@ -590,9 +596,12 @@ jobs:
                 echo "| $module_name | Z3 | BMC+prove | PASS |" >> $GITHUB_STEP_SUMMARY
               else
                 echo "| $module_name | Z3 | BMC+prove | FAIL/UNKNOWN |" >> $GITHUB_STEP_SUMMARY
-                echo "::warning::Formal verification of $module_name did not pass"
+                echo "::error::Formal verification of $module_name did not pass"
+                formal_failed=1
               fi
             done
+            # A refusal on the record beats a vacuous green (repo doctrine, NOW.md).
+            [ "${formal_failed:-0}" = "1" ] && exit 1
           else
             echo "| (all) | SymbiYosys not installed | - | SKIPPED |" >> $GITHUB_STEP_SUMMARY
             echo "::warning::SymbiYosys (sby) not available, formal check skipped"
@@ -690,7 +699,9 @@ jobs:
             # has non-constant args synthesis cannot evaluate (mac.v:535). As
             # written, this loop could never have passed.
             name=$(sed -n 's/^module \([A-Za-z0-9_]*\).*/\1/p' "$v" | head -1)
-            if iverilog -o "build/fpga/conformance/${name}_tb.vvp" -g2005 "$v" 2>/dev/null; then
+            # Audit 2026-08-19: bare -g2005 compiled 0/32 -- the repo convention
+            # (-sv -DSIMULATION, same fix as the yosys loop) was never applied here.
+            if iverilog -o "build/fpga/conformance/${name}_tb.vvp" -g2012 -DSIMULATION "$v" 2>/dev/null; then
               pass=$((pass+1))
             else
               fail=$((fail+1))
@@ -704,7 +715,8 @@ jobs:
           echo "| Total | $total |" >> $GITHUB_STEP_SUMMARY
           echo "" >> $GITHUB_STEP_SUMMARY
           if [ "$fail" -gt 0 ]; then
-            echo "::warning::$fail/$total modules failed iverilog compilation"
+            echo "::error::$fail/$total modules failed iverilog compilation"
+            exit 1
           fi
 
       - name: Validate conformance JSON structure

bootstrap/src/main.rs

@@ -10469,6 +10469,10 @@ fn run_synth_readiness(specs_dir: &str) -> anyhow::Result<()> {
         println!("\nALMOST READY — test coverage needs improvement");
     } else {
         println!("\nNOT READY — fix parse/verilog errors first");
+        // Audit 2026-08-19: this verdict printed for months while the step stayed
+        // green -- the binary always exited 0. A verdict that gates nothing is a
+        // caption, not a check.
+        anyhow::bail!("synth-readiness: NOT READY");
     }
 
     Ok(())

contrib/formal/fifo_formal.sby

@@ -1,23 +1,25 @@
+# Audit 2026-08-19: the old file used indented pseudo-blocks after 'bmc:'/'prove:',
+# which sby does not parse as task conditionals -- the bmc task saw no [engines]
+# and died with 'Config file is lacking engine configuration' on every run. Task
+# conditionals in sby are per-line 'task: option'. Paths were ../../../specs/fpga/
+# which escapes the workspace; the workflow copies the generated .v NEXT TO this file.
 [tasks]
 bmc
 prove
 
 [options]
-bmc:
-  mode bmc
-  depth 30
-prove:
-  mode prove
-  depth 30
+bmc: mode bmc
+prove: mode prove
+depth 30
 
 [engines]
 smtbmc z3
 
 [script]
-read_verilog -formal ../../../specs/fpga/fifo.v
+read_verilog -formal fifo.v
 read_verilog fifo_formal_props.v
 prep -top fifo_formal_props
 
 [files]
-../../../specs/fpga/fifo.v
+fifo.v
 fifo_formal_props.v

contrib/formal/mac_formal.sby

@@ -1,21 +1,25 @@
+# Audit 2026-08-19: the old file used indented pseudo-blocks after 'bmc:'/'prove:',
+# which sby does not parse as task conditionals -- the bmc task saw no [engines]
+# and died with 'Config file is lacking engine configuration' on every run. Task
+# conditionals in sby are per-line 'task: option'. Paths were ../../../specs/fpga/
+# which escapes the workspace; the workflow copies the generated .v NEXT TO this file.
 [tasks]
 bmc
 prove
 
 [options]
-bmc:
-  mode bmc
-  depth 20
-prove:
-  mode prove
-  depth 20
+bmc: mode bmc
+prove: mode prove
+depth 20
 
 [engines]
 smtbmc z3
 
 [script]
-read_verilog -formal ../../../specs/fpga/mac.v
-prep -top ZeroDSP_MAC
+read_verilog -formal mac.v
+read_verilog mac_formal_props.v
+prep -top mac_formal_props
 
 [files]
-../../../specs/fpga/mac.v
+mac.v
+mac_formal_props.v

contrib/formal/uart_formal.sby

@@ -1,19 +1,19 @@
+# Audit 2026-08-19: see fifo_formal.sby header -- same two defects fixed.
 [tasks]
 bmc
 
 [options]
-bmc:
-  mode bmc
-  depth 50
+mode bmc
+depth 50
 
 [engines]
 smtbmc z3
 
 [script]
-read_verilog -formal ../../../specs/fpga/uart.v
+read_verilog -formal uart.v
 read_verilog uart_formal_props.v
 prep -top uart_formal_props
 
 [files]
-../../../specs/fpga/uart.v
+uart.v
 uart_formal_props.v

docs/NOW.md

@@ -1,3 +1,25 @@
+# NOW -- the vacuous greens are gates again (2026-08-19)
+
+Last updated: 2026-08-19
+
+## ci(fpga)+fix: formal/conformance/lint/readiness now fail when they find nothing (Closes #2239)
+
+- Adversarial self-audit over the green master run (each finding survived two
+  independent refutation passes): fpga-formal verified ZERO properties (sby
+  pseudo-block configs + workspace-escaping paths + missing pipefail + a
+  continue-on-error cap -- three independent layers each guaranteeing green);
+  fpga-conformance compiled 0/32 (bare -g2005) behind a warning, and never runs
+  vvp at all (#2241); fpga-lint absorbed 'NOT READY' and 1/32 invalid Verilog
+  as warnings
+- Fixed: canonical per-line .sby task conditionals + local [files] paths;
+  set -o pipefail + continue-on-error removed + FAIL fails; iverilog -g2012
+  -DSIMULATION + exit 1; lint exit 1; synth-readiness bails on NOT READY
+- These jobs may now go honestly red on master: the lint red has a named cause
+  -- a live gen-verilog regression gluing a struct-field onto a part-select in
+  fifo.v (#2240), absorbed by the old warning-gate 40 minutes after the 32/32
+  claim. A refusal on the record beats a vacuous green
+
+
 # NOW -- the tri CLI wave lands: mutate, pr ready, synth/sweep area (2026-08-20)
 
 Last updated: 2026-08-20