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

* NNV_CONV_TRUST_FP32: clean 0/1 toggle + ship-policy documentation (competition behavior UNCHANGED)

Decision (Taylor): SHIP with the FP32 conv-screen unsat-emit ON for the competition (governs ~80
breadth-pts of cifar/tinyimagenet unsats; the FP64 reconfirm is too slow at the 100s budget). To make
it explorable post-competition:
- CONFIGURABILITY: replace the ~isempty(getenv(...)) footgun (where  did NOT disable -- any
  non-empty value counted as ON) with a clean i_envon() boolean: =1/true/on -> ON, =0/unset -> OFF
  (-> the sound FP64 double-confirm). Competition env sets =1 -> behavior IDENTICAL. Verified:
  i_envon('1')=1, ('0')=0, (unset)=0, ('true')=1, (' 1 ')=1, ('foo')=0; static analyzer clean.
- DOCUMENTATION: CONV_TRUST_FP32_POLICY.md (what it does, the αβ-CROWN/NeuralSAT-equivalent soundness
  basis, the 0-false-robust gold-set validation + the overnight FP64 double-oracle on the 5 thin-margin
  cases, what rides on it, the toggle, and the post-competition paths: sound-FP32 emit, FP64-only,
  matmul measured-δ). Plus an inline env-file comment.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015S5FFjy7MeJdSSovzjC6yw

* address Copilot feedback on #444: apply i_envon to NNV_SOUND_FP32_TIGHT + NNV_CONV_NO_STAR (same footgun); reword external status-repo refs

- NNV_SOUND_FP32_TIGHT and NNV_CONV_NO_STAR also used ~isempty(getenv(...)) so =0 wouldn't disable;
  now clean i_envon() toggles (competition sets =1 -> unchanged). NNV_PHASE_LOG/DEBUG left as-is
  (those are path-SET checks, not booleans).
- CONV_TRUST_FP32_POLICY.md: clarified the status-repo/ paths are in the team's SEPARATE internal
  status-tracking repo, not this nnv repo (dangling-ref note).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015S5FFjy7MeJdSSovzjC6yw

---------

Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

Author: ttj

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

@@ -0,0 +1,53 @@
+# 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). [Evidence lives in the team's SEPARATE internal status-tracking repo
+  (not this nnv 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 (documented in the
+   team's separate internal status-tracking 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,8 +1152,11 @@ 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'));
-            soundEmit = ~isempty(getenv('NNV_SOUND_FP32_TIGHT'));     % sound-FP32 fast-emit attempt enabled
+            % 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 = i_envon('NNV_SOUND_FP32_TIGHT');             % sound-FP32 fast-emit attempt enabled (clean 1/0 toggle, like TRUST_FP32)
             screenPass = true;
             if useScreen
                 % FAST UNSOUND-FP32 SCREEN: the cheap, TIGHT candidate filter. soundFP32=false FORCES it
@@ -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;
@@ -1216,7 +1219,7 @@ function i_log_cpstar(onnx)
             % whose Star provably never certifies), malbeware's approx/exact-star ladder DOES decide
             % instances (esp. the linear-25 FC net). Stripping it would regress the 88 baseline. So a
             % non-certified malbeware instance keeps its sound Star fallback (strictly additive).
-            if status == 2 && ~isempty(getenv('NNV_CONV_NO_STAR')) && ~contains(category,"malbeware")
+            if status == 2 && i_envon('NNV_CONV_NO_STAR') && ~contains(category,"malbeware")
                 reachOptionsList = {};
                 fprintf('GPU-BaB pre-check: conv not certified + NNV_CONV_NO_STAR -> skip Star (fast unknown)\n');
             end
@@ -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.