NNV_CONV_TRUST_FP32: clean 0/1 toggle + ship-policy docs (competition behavior unchanged)

code/nnv/examples/Submission/VNN_COMP2026/CONV_TRUST_FP32_POLICY.md

@@ -0,0 +1,51 @@
+# NNV_CONV_TRUST_FP32 — conv unsat-emit soundness policy
+
+**Decision (Taylor, 2026-06-28): SHIP WITH IT ON for VNN-COMP 2026.** This doc records what the
+policy is, why it is sound enough to ship, exactly what rides on it, how to toggle it, and the
+post-competition exploration paths.
+
+## What it does
+For conv nets (cifar100, tinyimagenet, vggnet), NNV runs a **GPU-single FP32 batched-BaB "screen"**
+(a raw CROWN lower bound on the spec margin, run entirely on the GPU). When the screen certifies
+`robust` AND the falsify-first PGD attack found no counterexample, NNV **emits `unsat` directly from
+the screen** and skips the ~120–194s FP64-CPU double-confirm. (`run_vnncomp_instance.m`, the
+`i_gpu_bab_precheck` conv branch.)
+
+## Why it is sound enough to ship (but is NOT a rigorous FP64 proof)
+- **Two-mechanism model.** A `robust` FP32 lower bound + an independent adversarial attack (PGD)
+  finding nothing is exactly the soundness model the GPU-winning tools use: **α,β-CROWN runs stock
+  FP32 with PGD; NeuralSAT likewise.** We are not doing anything more aggressive than the field SOTA.
+- **The FP32 rounding gap is ~1e-6**, far below the real robustness margins on these nets (the
+  overnight P2 analysis measured intrinsic margins 1.4e-4 … 0.042; the thin-margin cifar recoveries
+  have FP64 margins like +0.042).
+- **Validated 0-false-robust** vs the α,β-CROWN gold set (23 cifar100/tinyimagenet incl gold-SAT).
+- **Overnight defense-in-depth (2026-06-28):** the 5 thin-margin cifar resnet_large recoveries
+  (idx 496/4385/5308/4757/8589) were independently **FP64 double-oracle confirmed** robust (unsat via
+  3/7/15/9/175-node double; `status-repo/research/cifar_fp64_goldgate_2026-06-27/`).
+- **Residual risk (honest):** it is NOT an FP64 proof. If FP32 rounding ever flips a real margin on an
+  instance PGD also misses → a false unsat → −150. The above evidence bounds, but does not eliminate,
+  that risk. This is the standard FP32-verifier risk the whole field accepts.
+
+## What rides on it
+Essentially **all of cifar100's ~42% and tinyimagenet's ~40%** (≈ **80 breadth-points**) — their
+unsats exist only via this path. Turning it OFF reverts them to `unknown`, because the sound FP64
+reconfirm (120–194s) exceeds the 100s budget. So the choice is "ship the field-standard FP32 policy"
+vs "≈0 conv unsats".
+
+## How to toggle it (configurable, clean)
+`NNV_CONV_TRUST_FP32` is now a **clean boolean** (via `i_envon()` in run_vnncomp_instance.m):
+- `=1` / `true` / `on` / `yes` → **ON** (competition default; `vnncomp2026_env.sh`).
+- `=0` / `false` / anything else / **unset** → **OFF** → conv goes straight to the sound FP64 double-confirm.
+- (Historical footgun, fixed 2026-06-28: it used to read `~isempty(getenv(...))`, so `=0` did NOT
+  disable — any non-empty value, including the string `'0'`, counted as ON.)
+
+## Post-competition exploration paths (for tightening the soundness story)
+1. **Broader FP64 verification (free, no risk):** run the FP64 double-oracle (set `NNV_CONV_TRUST_FP32=0`,
+   generous timeout) over ALL conv unsats, not just the 5 — confirm 0 disagreements with the screen.
+2. **Sound-FP32 emit (`NNV_SOUND_FP32_TIGHT`, default OFF):** the outward-rounded FP32 path — a provably
+   sound lower bound (every CROWN bound widened by a rigorous roundoff bound) emitted from the GPU. The
+   blocker is that the worst-case Higham γ_n widening is too loose on the wide-conv matmul; the
+   **matmul measured-δ** (running-error analysis) is the lever to make it tight (see
+   `status-repo/memory conv-sound-emit-diagnosis`, SUPERVISED-only, −150-sensitive).
+3. **FP64-only (maximally conservative):** `NNV_CONV_TRUST_FP32=0`. Sound, but loses ~80 breadth-points
+   at the 100s budget unless the FP64 confirm is sped up (the matmul-δ / batched-double work).

code/nnv/examples/Submission/VNN_COMP2026/run_vnncomp_instance.m

@@ -1152,7 +1152,10 @@ function i_log_cpstar(onnx)
             % NNV_CONV_TRUST_FP32 emits FROM the GPU-single screen, so it FORCES the screen on (else
             % NNV_CONV_GPU_SCREEN=0 from FIX A1 would skip the screen -> straight to the FP64-CPU
             % confirm and trust-FP32 could never fire / the GPU would stay idle).
-            useScreen = ~isequal(getenv('NNV_CONV_GPU_SCREEN'), '0') || ~isempty(getenv('NNV_CONV_TRUST_FP32'));
+            % CONFIGURABILITY: i_envon() is a clean boolean toggle -- NNV_CONV_TRUST_FP32=1 ON, =0 (or
+            % unset) OFF -> straight to the sound FP64-double confirm. (Was ~isempty(), a footgun where
+            % `=0` did NOT disable -- any non-empty value counted as ON. See CONV_TRUST_FP32_POLICY.md.)
+            useScreen = ~isequal(getenv('NNV_CONV_GPU_SCREEN'), '0') || i_envon('NNV_CONV_TRUST_FP32');
             soundEmit = ~isempty(getenv('NNV_SOUND_FP32_TIGHT'));     % sound-FP32 fast-emit attempt enabled
             screenPass = true;
             if useScreen
@@ -1178,7 +1181,7 @@ function i_log_cpstar(onnx)
                 % rounding (~1e-6, negligible vs real robustness margins) instead of the rigorous FP64
                 % confirm; gated OFF by default and to be validated 0 false-robust vs the alpha-beta-CROWN
                 % gold set before competition use. PGD is the backstop for the residual FP32 gap.
-                if useScreen && ~isempty(getenv('NNV_CONV_TRUST_FP32'))
+                if useScreen && i_envon('NNV_CONV_TRUST_FP32')
                     status = 1; reachOptionsList = {};
                     fprintf('GPU-BaB pre-check: robust/unsat (TRUSTED gpu-single screen, %d nodes; PGD falsify-first clean) -> skip Star\n', ginfo.nodes);
                     return;
@@ -2649,4 +2652,12 @@ function delete_if_exists(f)
     else
         error("InputSize = "+string(s));
     end
+end
+
+function tf = i_envon(name)
+% Clean boolean env toggle: TRUE iff getenv(name) is a truthy token (1/true/on/yes, case-
+% insensitive); '0'/'false'/'off'/'no'/'' (or unset) -> FALSE. This lets `NAME=0` cleanly
+% DISABLE a flag, instead of the ~isempty() footgun where ANY non-empty value (including the
+% string '0') counted as ON. Used for NNV_CONV_TRUST_FP32 -- see CONV_TRUST_FP32_POLICY.md.
+    tf = any(strcmpi(strtrim(getenv(name)), {'1','true','on','yes'}));
 end

code/nnv/examples/Submission/VNN_COMP2026/vnncomp2026_env.sh

@@ -19,6 +19,12 @@
 #   GPU, ~5x faster than the FP64-CPU reconfirm), PGD falsify-first as the backstop -- the same two-mechanism
 #   model alpha-beta-CROWN / NeuralSAT use. Validated 0 false-robust vs the alpha-beta-CROWN gold set
 #   (23 cifar100/tinyimagenet incl gold-SAT). Forces the GPU screen ON. WITHOUT it -> 0 conv unsats.
+#   SHIPPING POLICY (Taylor, 2026-06-28): KEEP ON for the competition. It governs ~all of cifar100's 42%
+#   and tinyimagenet's 40% (~80 breadth-pts); turning it OFF reverts those to unknown (the sound FP64
+#   reconfirm is 120-194s, over the 100s budget). SOUNDNESS basis + the post-competition exploration paths
+#   (sound-FP32 emit NNV_SOUND_FP32_TIGHT, FP64-only, matmul measured-delta) are in CONV_TRUST_FP32_POLICY.md.
+#   CONFIGURABLE: a CLEAN toggle now -- =1 ON, =0 (or unset) OFF -> straight to the sound FP64 double-confirm.
+#   (Was a footgun: `=0` did NOT disable; it read non-empty=ON. Fixed via i_envon() in run_vnncomp_instance.m.)
 export NNV_CONV_TRUST_FP32=1
 # NNV_CONV_NO_STAR: a non-certifying conv precheck emits a FAST sound 'unknown' (Star never certifies these
 #   resnets, it just burns the whole timeout). WITHOUT it -> every conv instance times out.