refactor(back_end): retire 13 uncollected self-tests behind two CI gates

.codecov.yml

@@ -14,7 +14,7 @@ coverage:
   status:
     project:
       default:
-        target: 74%
+        target: 75%
         threshold: 1%
         informational: false
     patch:

.github/workflows/act-bab.yml

@@ -231,6 +231,29 @@ jobs:
           coverage run -p -m act.back_end --verify --network act/back_end/examples/nets/layer_testing_bab_deep.json \
             --solver dual --method planar --device cpu --dtype float64
 
+      # ===================================================================
+      # Soundness gate: a BaB run that exhausts its node budget with unproven
+      # sub-boxes left in the pool MUST report UNKNOWN, never CERTIFIED. Every
+      # other step here asserts throughput (node counts, exit codes); this is
+      # the only one asserting the verifier does not claim more than it proved.
+      #
+      # layer_testing_bab_deep is certified by presolve and never branches, so
+      # it cannot exhaust anything -- mlp_plain_3x8 is the net that survives
+      # presolve and enters BaB. --verbose is load-bearing: backend_cli only
+      # prints result.metadata under it.
+      # ===================================================================
+      - name: BaB soundness — budget exhaustion returns UNKNOWN
+        run: |
+          cd ${{ github.workspace }}
+          out=$(coverage run -p -m act.back_end --verify \
+            --network "$ACT_NETS_DIR/mlp_plain_3x8_64x64_3962224133.json" \
+            --bab --bab-max-depth 10 --bab-max-subproblems 2 --bab-max-batch-size 1 \
+            --solver torchlp --device cpu --dtype float64 --verbose 2>&1)
+          echo "$out"
+          grep -q "Lane 0: VerifyStatus.UNKNOWN"                      <<<"$out"
+          grep -q "reason: budget_exhausted_with_unproven_subboxes"   <<<"$out"
+          grep -q "exhausted_budget_nodes: True"                      <<<"$out"
+
       # ===================================================================
       # Dual MATMUL bilinear kernel (tf_transformer): dual-tier soundness on
       # the MATMUL layer-testing net (torchlp sweep never exercises dual here).

.github/workflows/act-backend-float32.yml

@@ -60,10 +60,13 @@ jobs:
           cd ${{ github.workspace }}
           coverage run -p -m act.pipeline --verify act2torch --device cpu --dtype float32
 
-      - name: Run Verifier Self-Tests (float32)
+      - name: Constraint exporter — torchlp LP export over all layer_testing nets
         run: |
           cd ${{ github.workspace }}
-          coverage run -p -m act.back_end.verifier
+          for f in act/back_end/examples/nets/layer_testing_*.json; do
+            coverage run -p -m act.back_end --verify --network "$f" \
+              --solver torchlp --device cpu --dtype float32
+          done
 
       # ─────────────────────────────────────────────────────────────────
       # Soundness check (TF-agnostic): runs once before per-solver matrix.

.github/workflows/act-backend-float64.yml

@@ -65,10 +65,13 @@ jobs:
           cd ${{ github.workspace }}
           coverage run -p -m act.pipeline --verify act2torch --device cpu --dtype float64
 
-      - name: Run Verifier Self-Tests (float64)
+      - name: Constraint exporter — torchlp LP export over all layer_testing nets
         run: |
           cd ${{ github.workspace }}
-          coverage run -p -m act.back_end.verifier
+          for f in act/back_end/examples/nets/layer_testing_*.json; do
+            coverage run -p -m act.back_end --verify --network "$f" \
+              --solver torchlp --device cpu --dtype float64
+          done
 
       # ─────────────────────────────────────────────────────────────────
       # Soundness check (TF-agnostic): runs once before per-solver matrix.